ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_2<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set M<VAR>H : ∀ t ⊆ s, t.Finite → LinearIndependent R fun (x : ↑t) => ↑x<GOAL>LinearIndependent R fun (x : ↑s) => ↑x
<VAR>R : Type u_2<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>η : Type u_8<VAR>s : η → Set M<VAR>hs : Directed (fun x x_1 => x ⊆ x_1) s<VAR>h : ∀ (i : η), LinearIndependent R fun (x : ↑(s i)) => ↑x<GOAL>LinearIndependent R fun (x : ↑(⋃ i, s i)) => ↑x
<VAR>R : Type u_2<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set (Set M)<VAR>hs : DirectedOn (fun x x_1 => x ⊆ x_1) s<VAR>h : ∀ a ∈ s, LinearIndependent (ι := { x // x ∈ a }) R Subtype.val<GOAL>LinearIndependent R fun (x : ↑(⋃₀ s)) => ↑x
<VAR>R : Type u_2<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>η : Type u_8<VAR>s : Set η<VAR>t : η → Set M<VAR>hs : DirectedOn (t ⁻¹'o fun x x_1 => x ⊆ x_1) s<VAR>h : ∀ a ∈ s, LinearIndependent R fun (x : ↑(t a)) => ↑x<GOAL>LinearIndependent R fun (x : ↑(⋃ a ∈ s, t a)) => ↑x
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>v : ι → M<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<GOAL>LinearIndependent R v ↔ Function.Injective ⇑(Finsupp.total ι M R v)
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>v : ι → M<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>Nontrivial R<VAR>hv : LinearIndependent R v<GOAL>Function.Injective v
<VAR>R : Type u_2<VAR>M : Type u_4<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_8<VAR>f : ι → M<VAR>hf : LinearIndependent R f<GOAL>LinearIndependent (ι := { x // x ∈ Set.range f }) R Subtype.val
<VAR>R : Type u_2<VAR>M : Type u_4<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_8<VAR>f : ι → M<VAR>hf : LinearIndependent R f<VAR>t : Set M<VAR>ht : Set.range f = t<GOAL>LinearIndependent (ι := { x // x ∈ t }) R Subtype.val
<VAR>R : Type u_2<VAR>M : Type u_4<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>s : Set ι<VAR>f : ι → ι'<VAR>g : ι' → M<VAR>hs : LinearIndependent R fun (x : ↑s) => g (f ↑x)<GOAL>LinearIndependent R fun (x : ↑(f '' s)) => g ↑x
<VAR>R : Type u_2<VAR>M : Type u_4<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_8<VAR>s : Set ι<VAR>f : ι → M<VAR>hs : LinearIndependent R fun (x : ↑s) => f ↑x<GOAL>LinearIndependent R fun (x : ↑(f '' s)) => ↑x
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>G : Type u_8<VAR>hG : Group G<VAR>DistribMulAction G R<VAR>DistribMulAction G M<VAR>IsScalarTower G R M<VAR>SMulCommClass G R M<VAR>v : ι → M<VAR>hv : LinearIndependent R v<VAR>w : ι → G<GOAL>LinearIndependent R (w • v)
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>v : ι → M<VAR>hv : LinearIndependent R v<VAR>w : ι → Rˣ<GOAL>LinearIndependent R (w • v)
<VAR>R : Type u_2<VAR>M : Type u_4<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>x y : M<VAR>h : LinearIndependent R ![x, y]<VAR>s t s' t' : R<VAR>h' : s • x + t • y = s' • x + t' • y<GOAL>s = s' ∧ t = t'
<VAR>R : Type u_2<VAR>M : Type u_4<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>x y : M<VAR>h : LinearIndependent R ![x, y]<VAR>s t : R<VAR>h' : s • x = t • y<GOAL>s = 0 ∧ t = 0
<VAR>R : Type u_8<VAR>M : Type u_9<VAR>CommRing R<VAR>NoZeroDivisors R<VAR>AddCommGroup M<VAR>Module R M<VAR>x y : M<VAR>h : LinearIndependent R ![x, y]<VAR>a b c d : R<VAR>h' : a * d - b * c ≠ 0<GOAL>LinearIndependent R ![a • x + b • y, c • x + d • y]
<VAR>ι : Type w<VAR>R : Type u<VAR>Ring R<VAR>Nontrivial R<VAR>M : Type v<VAR>AddCommGroup M<VAR>Module R M<VAR>v : ι → M<VAR>i : LinearIndependent R v<GOAL>i.Maximal ↔ ∀ (κ : Type v) (w : κ → M), LinearIndependent R w → ∀ (j : ι → κ), w ∘ j = v → Function.Surjective j
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>Ring R<VAR>M : Type u_8<VAR>AddCommGroup M<VAR>Module R M<VAR>v : ι → M<VAR>li : LinearIndependent R v<VAR>c d : R<VAR>i j : ι<VAR>hc : c ≠ 0<VAR>h : c • v i = d • v j<GOAL>i = j
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>v : ι → M<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>hv : LinearIndependent R v<VAR>s t : Set ι<VAR>hs : Disjoint s t<GOAL>Disjoint (Submodule.span R (v '' s)) (Submodule.span R (v '' t))
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>v : ι → M<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>Nontrivial R<VAR>hv : LinearIndependent R v<VAR>s : Set ι<VAR>x : ι<VAR>h : x ∉ s<GOAL>v x ∉ Submodule.span R (v '' s)
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>v : ι → M<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>Nontrivial R<VAR>hv : LinearIndependent R v<VAR>x : ι<VAR>f : ι →₀ R<VAR>h : x ∉ f.support<GOAL>(Finsupp.total ι M R v) f ≠ v x
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>M : Type u_4<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>v : ι ⊕ ι' → M<GOAL>LinearIndependent R v ↔ LinearIndependent R (v ∘ Sum.inl) ∧ LinearIndependent R (v ∘ Sum.inr) ∧ Disjoint (Submodule.span R (Set.range (v ∘ Sum.inl))) (Submodule.span R (Set.range (v ∘ Sum.inr)))
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>M : Type u_4<VAR>v : ι → M<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>v' : ι' → M<VAR>hv : LinearIndependent R v<VAR>hv' : LinearIndependent R v'<VAR>h : Disjoint (Submodule.span R (Set.range v)) (Submodule.span R (Set.range v'))<GOAL>LinearIndependent R (Sum.elim v v')
<VAR>R : Type u_2<VAR>M : Type u_4<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>s t : Set M<VAR>hs : LinearIndependent R fun (x : ↑s) => ↑x<VAR>ht : LinearIndependent R fun (x : ↑t) => ↑x<VAR>hst : Disjoint (Submodule.span R s) (Submodule.span R t)<GOAL>LinearIndependent R fun (x : ↑(s ∪ t)) => ↑x
<VAR>R : Type u_2<VAR>M : Type u_4<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_8<VAR>f : ι → Set M<VAR>hl : ∀ (i : ι), LinearIndependent R fun (x : ↑(f i)) => ↑x<VAR>hd : ∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (Submodule.span R (f i)) (⨆ i ∈ t, Submodule.span R (f i))<GOAL>LinearIndependent R fun (x : ↑(⋃ i, f i)) => ↑x
<VAR>R : Type u_2<VAR>M : Type u_4<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>η : Type u_8<VAR>ιs : η → Type u_9<VAR>f : (j : η) → ιs j → M<VAR>hindep : ∀ (j : η), LinearIndependent R (f j)<VAR>hd : ∀ (i : η) (t : Set η), t.Finite → i ∉ t → Disjoint (Submodule.span R (Set.range (f i))) (⨆ i ∈ t, Submodule.span R (Set.range (f i)))<GOAL>LinearIndependent R fun ji => f ji.fst ji.snd
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>v : ι → M<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>hv : LinearIndependent R v<GOAL>∀ (a : ↥(Submodule.span R (Set.range v))), hv.totalEquiv.symm a = ((LinearEquiv.ofInjective (LinearMap.codRestrict (Submodule.span R (Set.range v)) (Finsupp.total ι M R v) ⋯) ⋯).toEquiv.trans (LinearEquiv.ofTop (LinearMap.range (LinearMap.codRestrict (Submodule.span R (Set.range v)) (Finsupp.total ι M R v) ⋯)) ⋯).toEquiv).invFun a
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>v : ι → M<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>hv : LinearIndependent R v<VAR>l : ι →₀ R<GOAL>↑(hv.totalEquiv l) = (Finsupp.total ι M R v) l
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>v : ι → M<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>hv : LinearIndependent R v<VAR>x : ↥(Submodule.span R (Set.range v))<GOAL>(Finsupp.total ι M R v) (hv.repr x) = ↑x
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>v : ι → M<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>hv : LinearIndependent R v<GOAL>Finsupp.total ι M R v ∘ₗ hv.repr = (Submodule.span R (Set.range v)).subtype
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>v : ι → M<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>hv : LinearIndependent R v<GOAL>LinearMap.ker hv.repr = ⊥
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>v : ι → M<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>hv : LinearIndependent R v<GOAL>LinearMap.range hv.repr = ⊤
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>v : ι → M<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>hv : LinearIndependent R v<VAR>l : ι →₀ R<VAR>x : ↥(Submodule.span R (Set.range v))<VAR>eq : (Finsupp.total ι M R v) l = ↑x<GOAL>hv.repr x = l
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>v : ι → M<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>hv : LinearIndependent R v<VAR>i : ι<VAR>x : ↥(Submodule.span R (Set.range v))<VAR>hx : ↑x = v i<GOAL>hv.repr x = Finsupp.single i 1
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>v : ι → M<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>hv : LinearIndependent R v<VAR>Nontrivial R<VAR>x : ↥(Submodule.span R (Set.range v))<GOAL>Span.repr R (Set.range v) x = Finsupp.equivMapDomain (Equiv.ofInjective v ⋯) (hv.repr x)
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>v : ι → M<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<GOAL>LinearIndependent R v ↔ ∀ (i : ι) (a : R), a • v i ∈ Submodule.span R (v '' (Set.univ \ {i})) → a = 0
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>v : ι → M<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>hv : LinearIndependent R v<GOAL>CompleteLattice.Independent fun i => Submodule.span R {v i}
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>s : ι → M<GOAL>∃ I, (LinearIndependent R fun (x : ↑I) => s ↑x) ∧ ∀ (J : Set ι), I ⊆ J → (LinearIndependent R fun (x : ↑J) => s ↑x) → I = J
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>s : ι → M<GOAL>∃ I, (LinearIndependent R fun (x : ↑I) => s ↑x) ∧ ∀ i ∉ I, ∃ a, a ≠ 0 ∧ a • s i ∈ Submodule.span R (s '' I)
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>M : Type u_4<VAR>v : ι → M<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>Nontrivial R<VAR>hv : LinearIndependent R v<VAR>f : ι' ↪ ι<VAR>hss : Set.range v ⊆ ↑(Submodule.span R (Set.range (v ∘ ⇑f)))<GOAL>Function.Surjective ⇑f
<VAR>R : Type u_2<VAR>M : Type u_4<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>Nontrivial R<VAR>s t : Set M<VAR>hs : LinearIndependent R fun (x : ↑s) => ↑x<VAR>h : t ⊆ s<VAR>hst : s ⊆ ↑(Submodule.span R t)<GOAL>s = t
<VAR>R : Type u_2<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>Ring R<VAR>AddCommGroup M<VAR>AddCommGroup M'<VAR>Module R M<VAR>Module R M'<VAR>s : Set M<VAR>f : M →ₗ[R] M'<VAR>hs : LinearIndependent R fun (x : ↑s) => ↑x<VAR>hf_inj : Disjoint (Submodule.span R s) (LinearMap.ker f)<GOAL>LinearIndependent R fun (x : ↑(⇑f '' s)) => ↑x
<VAR>R : Type u_2<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>Ring R<VAR>AddCommGroup M<VAR>AddCommGroup M'<VAR>Module R M<VAR>Module R M'<VAR>s : Set M<VAR>t : Set M'<VAR>hs : LinearIndependent R fun (x : ↑s) => ↑x<VAR>ht : LinearIndependent R fun (x : ↑t) => ↑x<GOAL>LinearIndependent R fun (x : ↑(⇑(LinearMap.inl R M M') '' s ∪ ⇑(LinearMap.inr R M M') '' t)) => ↑x
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>Ring R<VAR>AddCommGroup M<VAR>AddCommGroup M'<VAR>Module R M<VAR>Module R M'<VAR>v : ι → M<VAR>v' : ι' → M'<VAR>hv : LinearIndependent R v<VAR>hv' : LinearIndependent R v'<GOAL>LinearIndependent R (Sum.elim (⇑(LinearMap.inl R M M') ∘ v) (⇑(LinearMap.inr R M M') ∘ v'))
<VAR>G : Type u_8<VAR>Monoid G<VAR>L : Type u_9<VAR>CommRing L<VAR>NoZeroDivisors L<GOAL>LinearIndependent L fun f => ⇑f
<VAR>K : Type u_8<VAR>M : Type u_9<VAR>L : Type u_10<VAR>CommSemiring K<VAR>Semiring M<VAR>Algebra K M<VAR>CommRing L<VAR>IsDomain L<VAR>Algebra K L<GOAL>LinearIndependent L AlgHom.toLinearMap
<VAR>K : Type u_8<VAR>M : Type u_9<VAR>L : Type u_10<VAR>CommRing K<VAR>Semiring M<VAR>Algebra K M<VAR>CommRing L<VAR>IsDomain L<VAR>Algebra K L<VAR>NoZeroSMulDivisors K L<GOAL>LinearIndependent K AlgHom.toLinearMap
<VAR>R : Type u_2<VAR>M : Type u_4<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>Nontrivial R<VAR>s t u : Set M<VAR>hl : LinearIndependent (ι := { x // x ∈ u }) R Subtype.val<VAR>hsu : s ⊆ u<VAR>htu : t ⊆ u<VAR>hst : Submodule.span R s ≤ Submodule.span R t<GOAL>s ⊆ t
<VAR>R : Type u_2<VAR>M : Type u_4<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>Nontrivial R<VAR>s t u : Set M<VAR>hl : LinearIndependent (ι := { x // x ∈ u }) R Subtype.val<VAR>hsu : s ⊆ u<VAR>htu : t ⊆ u<GOAL>Submodule.span R s ≤ Submodule.span R t ↔ s ⊆ t
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>Ring R<VAR>Nontrivial R<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>v : ι → M<VAR>Unique ι<GOAL>LinearIndependent R v ↔ v default ≠ 0
<VAR>R : Type u_2<VAR>M : Type u_4<VAR>Ring R<VAR>Nontrivial R<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>x : M<VAR>hx : x ≠ 0<GOAL>LinearIndependent R fun (x_1 : ↑{x}) => ↑x_1
<VAR>K : Type u_3<VAR>V : Type u<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>s : Set V<VAR>x y : V<GOAL>x ∈ Submodule.span K (insert y s) → x ∉ Submodule.span K s → y ∈ Submodule.span K (insert x s)
<VAR>ι : Type u'<VAR>K : Type u_3<VAR>V : Type u<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>v : ι → V<GOAL>LinearIndependent K v ↔ ∀ (i : ι), v i ∉ Submodule.span K (v '' (Set.univ \ {i}))
<VAR>K : Type u_3<VAR>V : Type u<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>s : Set V<VAR>x : V<VAR>hs : LinearIndependent K fun (b : ↑s) => ↑b<VAR>hx : x ∉ Submodule.span K s<GOAL>LinearIndependent K fun (b : ↑(insert x s)) => ↑b
<VAR>ι : Type u'<VAR>K : Type u_3<VAR>V : Type u<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>v : ι → V<VAR>x : V<GOAL>(LinearIndependent K fun o => o.casesOn' x v) ↔ LinearIndependent K v ∧ x ∉ Submodule.span K (Set.range v)
<VAR>ι : Type u'<VAR>K : Type u_3<VAR>V : Type u<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>v : ι → V<VAR>x : V<VAR>hv : LinearIndependent K v<VAR>hx : x ∉ Submodule.span K (Set.range v)<GOAL>LinearIndependent K fun o => o.casesOn' x v
<VAR>ι : Type u'<VAR>K : Type u_3<VAR>V : Type u<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>v : Option ι → V<GOAL>LinearIndependent K v ↔ LinearIndependent K (v ∘ some) ∧ v none ∉ Submodule.span K (Set.range (v ∘ some))
<VAR>K : Type u_3<VAR>V : Type u<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>ι : Type u_8<VAR>s : Set ι<VAR>a : ι<VAR>f : ι → V<VAR>has : a ∉ s<GOAL>(LinearIndependent K fun (x : ↑(insert a s)) => f ↑x) ↔ (LinearIndependent K fun (x : ↑s) => f ↑x) ∧ f a ∉ Submodule.span K (f '' s)
<VAR>K : Type u_3<VAR>V : Type u<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>s : Set V<VAR>x : V<VAR>hxs : x ∉ s<GOAL>(LinearIndependent K fun (b : ↑(insert x s)) => ↑b) ↔ (LinearIndependent K fun (b : ↑s) => ↑b) ∧ x ∉ Submodule.span K s
<VAR>K : Type u_3<VAR>V : Type u<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : ∀ (a : K), a • x ≠ y<GOAL>LinearIndependent (ι := { x_1 // x_1 ∈ {x, y} }) K Subtype.val
<VAR>K : Type u_3<VAR>V : Type u<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>x y : V<VAR>hx : x ≠ 0<GOAL>LinearIndependent K ![x, y] ↔ ∀ (a : K), a • x ≠ y
<VAR>K : Type u_3<VAR>V : Type u<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>x : V<VAR>n : ℕ<VAR>v : Fin n → V<GOAL>LinearIndependent K (Fin.cons x v) ↔ LinearIndependent K v ∧ x ∉ Submodule.span K (Set.range v)
<VAR>K : Type u_3<VAR>V : Type u<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>x : V<VAR>n : ℕ<VAR>v : Fin n → V<GOAL>LinearIndependent K (Fin.snoc v x) ↔ LinearIndependent K v ∧ x ∉ Submodule.span K (Set.range v)
<VAR>K : Type u_3<VAR>V : Type u<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>x : V<VAR>n : ℕ<VAR>v : Fin n → V<VAR>hv : LinearIndependent K v<VAR>hx : x ∉ Submodule.span K (Set.range v)<GOAL>LinearIndependent K (Fin.cons x v)
<VAR>K : Type u_3<VAR>V : Type u<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>n : ℕ<VAR>v : Fin (n + 1) → V<GOAL>LinearIndependent K v ↔ LinearIndependent K (Fin.tail v) ∧ v 0 ∉ Submodule.span K (Set.range (Fin.tail v))
<VAR>K : Type u_3<VAR>V : Type u<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>n : ℕ<VAR>v : Fin (n + 1) → V<GOAL>LinearIndependent K v ↔ LinearIndependent K (Fin.init v) ∧ v (Fin.last n) ∉ Submodule.span K (Set.range (Fin.init v))
<VAR>K : Type u_3<VAR>V : Type u<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>f : Fin 2 → V<GOAL>LinearIndependent K f ↔ f 1 ≠ 0 ∧ ∀ (a : K), a • f 1 ≠ f 0
<VAR>K : Type u_3<VAR>V : Type u<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>s t : Set V<VAR>hs : LinearIndependent (ι := { x // x ∈ s }) K Subtype.val<VAR>hst : s ⊆ t<GOAL>∃ b ⊆ t, s ⊆ b ∧ t ⊆ ↑(Submodule.span K b) ∧ LinearIndependent (ι := { x // x ∈ b }) K Subtype.val
<VAR>K : Type u_3<VAR>V : Type u<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>t : Set V<GOAL>∃ b ⊆ t, Submodule.span K b = Submodule.span K t ∧ LinearIndependent (ι := { x // x ∈ b }) K Subtype.val
<VAR>K : Type u_3<VAR>V : Type u<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>s t : Set V<VAR>hs : LinearIndependent K fun (x : ↑s) => ↑x<VAR>hst : s ⊆ t<GOAL>hs.extend hst ⊆ t
<VAR>K : Type u_3<VAR>V : Type u<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>s t : Set V<VAR>hs : LinearIndependent K fun (x : ↑s) => ↑x<VAR>hst : s ⊆ t<GOAL>s ⊆ hs.extend hst
<VAR>K : Type u_3<VAR>V : Type u<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>s t : Set V<VAR>hs : LinearIndependent K fun (x : ↑s) => ↑x<VAR>hst : s ⊆ t<GOAL>t ⊆ ↑(Submodule.span K (hs.extend hst))
<VAR>K : Type u_3<VAR>V : Type u<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>s t : Set V<VAR>hs : LinearIndependent K fun (x : ↑s) => ↑x<VAR>hst : s ⊆ t<GOAL>LinearIndependent (ι := { x // x ∈ hs.extend hst }) K Subtype.val
<VAR>K : Type u_3<VAR>V : Type u<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>s : Set V<VAR>t : Finset V<VAR>hs : LinearIndependent K fun (x : ↑s) => ↑x<VAR>hst : s ⊆ ↑(Submodule.span K ↑t)<GOAL>∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = t.card
<VAR>K : Type u_3<VAR>V : Type u<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>s t : Set V<VAR>ht : t.Finite<VAR>hs : LinearIndependent K fun (x : ↑s) => ↑x<VAR>hst : s ⊆ ↑(Submodule.span K t)<GOAL>∃ (h : s.Finite), h.toFinset.card ≤ ht.toFinset.card
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>M N : Submodule R S<VAR>m : ↥M<VAR>n : ↥N<GOAL>(M.mulMap N) (m ⊗ₜ[R] n) = ↑m * ↑n
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>M N : Submodule R S<GOAL>(Submodule.equivOpposite.symm (MulOpposite.op M)).mulMap (Submodule.equivOpposite.symm (MulOpposite.op N)) = ↑(MulOpposite.opLinearEquiv R) ∘ₗ N.mulMap M ∘ₗ ↑(TensorProduct.congr ((MulOpposite.opLinearEquiv R).symm.ofSubmodule' M) ((MulOpposite.opLinearEquiv R).symm.ofSubmodule' N) ≪≫ₗ TensorProduct.comm R ↥M ↥N)
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>M N : Submodule R S<VAR>hc : ∀ (m : ↥M) (n : ↥N), Commute ↑m ↑n<GOAL>N.mulMap M = M.mulMap N ∘ₗ ↑(TensorProduct.comm R ↥N ↥M)
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>M : Submodule R S<VAR>N : Submodule R S<VAR>M' : Submodule R S<VAR>hM : M' ≤ M<GOAL>M.mulMap N ∘ₗ LinearMap.rTensor (↥N) (Submodule.inclusion hM) = M'.mulMap N
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>M : Submodule R S<VAR>N N' : Submodule R S<VAR>hN : N' ≤ N<GOAL>M.mulMap N ∘ₗ LinearMap.lTensor (↥M) (Submodule.inclusion hN) = M.mulMap N'
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>M N M' N' : Submodule R S<VAR>hM : M' ≤ M<VAR>hN : N' ≤ N<GOAL>M.mulMap N ∘ₗ TensorProduct.map (Submodule.inclusion hM) (Submodule.inclusion hN) = M'.mulMap N'
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>M N : Submodule R S<GOAL>M.mulMap N = LinearMap.mul' R S ∘ₗ TensorProduct.mapIncl M N
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>M N : Submodule R S<GOAL>LinearMap.range (M.mulMap N) = M * N
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>M N : Submodule R S<VAR>m : ↥M<VAR>n : ↥N<GOAL>↑((M.mulMap' N) (m ⊗ₜ[R] n)) = ↑m * ↑n
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>M N : Submodule R S<GOAL>Function.Surjective ⇑(M.mulMap' N)
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>N : Submodule R S<VAR>y : R<VAR>n : ↥N<GOAL>N.lTensorOne' ((algebraMap R ↥⊥) y ⊗ₜ[R] n) = y • n
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>N : Submodule R S<VAR>n : ↥N<GOAL>N.lTensorOne' (1 ⊗ₜ[R] n) = n
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>N : Submodule R S<VAR>y : R<VAR>n : ↥N<GOAL>N.lTensorOne ((algebraMap R ↥⊥) y ⊗ₜ[R] n) = y • n
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>N : Submodule R S<VAR>n : ↥N<GOAL>N.lTensorOne (1 ⊗ₜ[R] n) = n
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>N : Submodule R S<VAR>n : ↥N<GOAL>N.lTensorOne.symm n = 1 ⊗ₜ[R] n
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>N : Submodule R S<GOAL>Submodule.mulMap 1 N = N.subtype ∘ₗ ↑N.lTensorOne
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>M : Submodule R S<VAR>y : R<VAR>m : ↥M<GOAL>M.rTensorOne' (m ⊗ₜ[R] (algebraMap R ↥⊥) y) = y • m
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>M : Submodule R S<VAR>m : ↥M<GOAL>M.rTensorOne' (m ⊗ₜ[R] 1) = m
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>M : Submodule R S<VAR>y : R<VAR>m : ↥M<GOAL>M.rTensorOne (m ⊗ₜ[R] (algebraMap R ↥⊥) y) = y • m
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>M : Submodule R S<VAR>m : ↥M<GOAL>M.rTensorOne (m ⊗ₜ[R] 1) = m
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>M : Submodule R S<VAR>m : ↥M<GOAL>M.rTensorOne.symm m = m ⊗ₜ[R] 1
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>M : Submodule R S<GOAL>M.mulMap 1 = M.subtype ∘ₗ ↑M.rTensorOne
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>M : Submodule R S<GOAL>TensorProduct.comm R ↥M ↥⊥ ≪≫ₗ M.lTensorOne = M.rTensorOne
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>M : Submodule R S<GOAL>TensorProduct.comm R ↥⊥ ↥M ≪≫ₗ M.rTensorOne = M.lTensorOne
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>M : Submodule R S<VAR>N : Submodule R S<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>m : ι → ↥M<GOAL>Submodule.mulLeftMap N m = M.mulMap N ∘ₗ LinearMap.rTensor (↥N) (Finsupp.total ι (↥M) R m) ∘ₗ ↑(TensorProduct.finsuppScalarLeft R (↥N) ι).symm
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>M : Submodule R S<VAR>N : Submodule R S<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>n : ι → ↥N<GOAL>M.mulRightMap n = M.mulMap N ∘ₗ LinearMap.lTensor (↥M) (Finsupp.total ι (↥N) R n) ∘ₗ ↑(TensorProduct.finsuppScalarRight R (↥M) ι).symm
<VAR>R : Type u<VAR>S : Type v<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>M N : Submodule R S<GOAL>N.mulMap M = M.mulMap N ∘ₗ ↑(TensorProduct.comm R ↥N ↥M)
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>f : M → N<VAR>x y : M<GOAL>f (x + y) = f x + f y + QuadraticMap.polar f x y
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>f g : M → N<VAR>x y : M<GOAL>QuadraticMap.polar (f + g) x y = QuadraticMap.polar f x y + QuadraticMap.polar g x y
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>f : M → N<VAR>x y : M<GOAL>QuadraticMap.polar (-f) x y = -QuadraticMap.polar f x y
<VAR>S : Type u_1<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Monoid S<VAR>DistribMulAction S N<VAR>f : M → N<VAR>s : S<VAR>x y : M<GOAL>QuadraticMap.polar (s • f) x y = s • QuadraticMap.polar f x y
<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>f : M → N<VAR>x y : M<GOAL>QuadraticMap.polar f x y = QuadraticMap.polar f y x