ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>n : Type u_2<VAR>𝕜 : Type u_4<VAR>Fintype n<VAR>RCLike 𝕜<VAR>DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.PosDef<VAR>i : n<GOAL>0 < ⋯.eigenvalues i
<VAR>n : Type u_2<VAR>𝕜 : Type u_4<VAR>Fintype n<VAR>RCLike 𝕜<VAR>DecidableEq n<VAR>M : Matrix n n 𝕜<VAR>hM : M.PosDef<GOAL>0 < M.det
<VAR>n : Type u_1<VAR>Fintype n<VAR>DecidableEq n<VAR>Q : QuadraticForm ℝ (n → ℝ)<VAR>hQ : (QuadraticMap.toMatrix' Q).PosDef<GOAL>QuadraticMap.PosDef Q
<VAR>n : Type u_1<VAR>Fintype n<VAR>DecidableEq n<VAR>Q : QuadraticForm ℝ (n → ℝ)<VAR>hQ : QuadraticMap.PosDef Q<GOAL>(QuadraticMap.toMatrix' Q).PosDef
<VAR>K : Type u<VAR>V : Type v<VAR>Ring K<VAR>StrongRankCondition K<VAR>AddCommGroup V<VAR>Module K V<VAR>Module.Free K V<VAR>ι : Type u_1<VAR>IsEmpty ι<VAR>hV : Module.rank K V = 0<VAR>i : ι<GOAL>(Basis.ofRankEqZero hV) i = 0
<VAR>K : Type u<VAR>V : Type v<VAR>Ring K<VAR>StrongRankCondition K<VAR>AddCommGroup V<VAR>Module K V<VAR>Module.Free K V<VAR>c : Cardinal.{v}<GOAL>c ≤ Module.rank K V ↔ ∃ s, #↑s = c ∧ LinearIndependent (ι := { x // x ∈ s }) K Subtype.val
<VAR>K : Type u<VAR>V : Type v<VAR>Ring K<VAR>StrongRankCondition K<VAR>AddCommGroup V<VAR>Module K V<VAR>Module.Free K V<VAR>n : ℕ<GOAL>↑n ≤ Module.rank K V ↔ ∃ s, s.card = n ∧ LinearIndependent (ι := { x // x ∈ ↑s }) K Subtype.val
<VAR>K : Type u<VAR>V : Type v<VAR>Ring K<VAR>StrongRankCondition K<VAR>AddCommGroup V<VAR>Module K V<VAR>Module.Free K V<GOAL>Module.rank K V ≤ 1 ↔ ∃ v₀, ∀ (v : V), ∃ r, r • v₀ = v
<VAR>K : Type u<VAR>V : Type v<VAR>Ring K<VAR>StrongRankCondition K<VAR>AddCommGroup V<VAR>Module K V<VAR>Module.Free K V<GOAL>Module.rank K V = 1 ↔ ∃ v₀, v₀ ≠ 0 ∧ ∀ (v : V), ∃ r, r • v₀ = v
<VAR>K : Type u<VAR>V : Type v<VAR>Ring K<VAR>StrongRankCondition K<VAR>AddCommGroup V<VAR>Module K V<VAR>s : Submodule K V<VAR>Module.Free K ↥s<GOAL>Module.rank K ↥s ≤ 1 ↔ ∃ v₀ ∈ s, s ≤ Submodule.span K {v₀}
<VAR>K : Type u<VAR>V : Type v<VAR>Ring K<VAR>StrongRankCondition K<VAR>AddCommGroup V<VAR>Module K V<VAR>s : Submodule K V<VAR>Module.Free K ↥s<GOAL>Module.rank K ↥s = 1 ↔ ∃ v₀ ∈ s, v₀ ≠ 0 ∧ s ≤ Submodule.span K {v₀}
<VAR>K : Type u<VAR>V : Type v<VAR>Ring K<VAR>StrongRankCondition K<VAR>AddCommGroup V<VAR>Module K V<VAR>s : Submodule K V<VAR>Module.Free K ↥s<GOAL>Module.rank K ↥s ≤ 1 ↔ ∃ v₀, s ≤ Submodule.span K {v₀}
<VAR>K : Type u<VAR>V : Type v<VAR>Ring K<VAR>StrongRankCondition K<VAR>AddCommGroup V<VAR>Module K V<VAR>W : Submodule K V<VAR>Module.Free K ↥W<GOAL>Module.rank K ↥W ≤ 1 ↔ W.IsPrincipal
<VAR>K : Type u<VAR>V : Type v<VAR>Ring K<VAR>StrongRankCondition K<VAR>AddCommGroup V<VAR>Module K V<VAR>Module.Free K V<GOAL>Module.rank K V ≤ 1 ↔ ⊤.IsPrincipal
<VAR>K : Type u<VAR>V : Type v<VAR>Ring K<VAR>StrongRankCondition K<VAR>AddCommGroup V<VAR>Module K V<VAR>Module.Free K V<VAR>ι : Type u_1<VAR>Unique ι<GOAL>FiniteDimensional.finrank K V = 1 ↔ Nonempty (Basis ι K V)
<VAR>K : Type u<VAR>V : Type v<VAR>Ring K<VAR>StrongRankCondition K<VAR>AddCommGroup V<VAR>Module K V<VAR>Module.Free K V<GOAL>FiniteDimensional.finrank K V = 1 ↔ ∃ v, v ≠ 0 ∧ ∀ (w : V), ∃ c, c • v = w
<VAR>K : Type u<VAR>V : Type v<VAR>Ring K<VAR>StrongRankCondition K<VAR>AddCommGroup V<VAR>Module K V<VAR>Module.Free K V<VAR>Module.Finite K V<GOAL>FiniteDimensional.finrank K V ≤ 1 ↔ ∃ v, ∀ (w : V), ∃ c, c • v = w
<VAR>K : Type u<VAR>V : Type v<VAR>Ring K<VAR>StrongRankCondition K<VAR>AddCommGroup V<VAR>Module K V<VAR>W : Submodule K V<VAR>Module.Free K ↥W<VAR>Module.Finite K ↥W<GOAL>FiniteDimensional.finrank K ↥W ≤ 1 ↔ W.IsPrincipal
<VAR>K : Type u<VAR>V : Type v<VAR>Ring K<VAR>StrongRankCondition K<VAR>AddCommGroup V<VAR>Module K V<VAR>Module.Free K V<VAR>Module.Finite K V<GOAL>FiniteDimensional.finrank K V ≤ 1 ↔ ⊤.IsPrincipal
<VAR>K : Type u<VAR>V : Type v<VAR>Ring K<VAR>StrongRankCondition K<VAR>AddCommGroup V<VAR>Module K V<VAR>Module.Free K V<VAR>Module.Finite K V<GOAL>Cardinal.lift.{u, v} #V = Cardinal.lift.{v, u} #K ^ Cardinal.lift.{u, v} (Module.rank K V)
<VAR>K V : Type u<VAR>Ring K<VAR>StrongRankCondition K<VAR>AddCommGroup V<VAR>Module K V<VAR>Module.Free K V<VAR>Module.Finite K V<GOAL>#V = #K ^ Module.rank K V
<VAR>K : Type u<VAR>V : Type v<VAR>Ring K<VAR>StrongRankCondition K<VAR>AddCommGroup V<VAR>Module K V<VAR>Finite K<VAR>Module.Free K V<VAR>Module.Finite K V<GOAL>#V < ℵ₀
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>CommRing F<VAR>StrongRankCondition F<VAR>Ring E<VAR>Algebra F E<VAR>S : Subalgebra F E<VAR>h : Module.rank F ↥S ≤ 1<VAR>Module.Free F ↥S<GOAL>S = ⊥
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>CommRing F<VAR>StrongRankCondition F<VAR>Ring E<VAR>Algebra F E<VAR>S : Subalgebra F E<VAR>h : FiniteDimensional.finrank F ↥S = 1<VAR>Module.Free F ↥S<GOAL>S = ⊥
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>CommRing F<VAR>StrongRankCondition F<VAR>Ring E<VAR>Algebra F E<VAR>S : Subalgebra F E<VAR>Nontrivial E<VAR>Module.Free F ↥S<GOAL>Module.rank F ↥S = 1 ↔ S = ⊥
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>CommRing F<VAR>StrongRankCondition F<VAR>Ring E<VAR>Algebra F E<VAR>S : Subalgebra F E<VAR>Nontrivial E<VAR>Module.Free F ↥S<GOAL>FiniteDimensional.finrank F ↥S = 1 ↔ S = ⊥
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>CommRing F<VAR>StrongRankCondition F<VAR>Ring E<VAR>Algebra F E<VAR>Nontrivial E<VAR>Module.Free F E<GOAL>⊥ = ⊤ ↔ Module.rank F E = 1
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>CommRing F<VAR>StrongRankCondition F<VAR>Ring E<VAR>Algebra F E<VAR>Nontrivial E<VAR>Module.Free F E<GOAL>⊥ = ⊤ ↔ FiniteDimensional.finrank F E = 1
<VAR>F : Type u<VAR>K : Type v<VAR>A : Type w<VAR>Ring F<VAR>Ring K<VAR>AddCommGroup A<VAR>Module F K<VAR>Module K A<VAR>Module F A<VAR>IsScalarTower F K A<VAR>StrongRankCondition F<VAR>StrongRankCondition K<VAR>Module.Free F K<VAR>Module.Free K A<GOAL>Cardinal.lift.{w, v} (Module.rank F K) * Cardinal.lift.{v, w} (Module.rank K A) = Cardinal.lift.{v, w} (Module.rank F A)
<VAR>F : Type u<VAR>K : Type v<VAR>Ring F<VAR>Ring K<VAR>Module F K<VAR>StrongRankCondition F<VAR>StrongRankCondition K<VAR>Module.Free F K<VAR>A : Type v<VAR>AddCommGroup A<VAR>Module K A<VAR>Module F A<VAR>IsScalarTower F K A<VAR>Module.Free K A<GOAL>Module.rank F K * Module.rank K A = Module.rank F A
<VAR>F : Type u<VAR>K : Type v<VAR>A : Type w<VAR>Ring F<VAR>Ring K<VAR>AddCommGroup A<VAR>Module F K<VAR>Module K A<VAR>Module F A<VAR>IsScalarTower F K A<VAR>StrongRankCondition F<VAR>StrongRankCondition K<VAR>Module.Free F K<VAR>Module.Free K A<GOAL>FiniteDimensional.finrank F K * FiniteDimensional.finrank K A = FiniteDimensional.finrank F A
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>StrongRankCondition R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<GOAL>Module.rank R M = #(Module.Free.ChooseBasisIndex R M)
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>StrongRankCondition R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<VAR>Module.Finite R M<GOAL>FiniteDimensional.finrank R M = Fintype.card (Module.Free.ChooseBasisIndex R M)
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>StrongRankCondition R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<VAR>Infinite R<VAR>h_lt : Cardinal.lift.{v, u} #R < Cardinal.lift.{u, v} #M<GOAL>Module.rank R M = #M
<VAR>R : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>Ring R<VAR>StrongRankCondition R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<VAR>AddCommGroup M'<VAR>Module R M'<VAR>Module.Free R M'<VAR>cnd : Cardinal.lift.{v', v} (Module.rank R M) = Cardinal.lift.{v, v'} (Module.rank R M')<GOAL>Nonempty (M ≃ₗ[R] M')
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>Ring R<VAR>StrongRankCondition R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<VAR>AddCommGroup M₁<VAR>Module R M₁<VAR>Module.Free R M₁<VAR>cond : Module.rank R M = Module.rank R M₁<GOAL>Nonempty (M ≃ₗ[R] M₁)
<VAR>R : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>Ring R<VAR>StrongRankCondition R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<VAR>AddCommGroup M'<VAR>Module R M'<VAR>Module.Free R M'<GOAL>Nonempty (M ≃ₗ[R] M') ↔ Cardinal.lift.{v', v} (Module.rank R M) = Cardinal.lift.{v, v'} (Module.rank R M')
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>Ring R<VAR>StrongRankCondition R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<VAR>AddCommGroup M₁<VAR>Module R M₁<VAR>Module.Free R M₁<GOAL>Nonempty (M ≃ₗ[R] M₁) ↔ Module.rank R M = Module.rank R M₁
<VAR>R : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>Ring R<VAR>StrongRankCondition R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<VAR>AddCommGroup M'<VAR>Module R M'<VAR>Module.Free R M'<VAR>Module.Finite R M<VAR>Module.Finite R M'<VAR>cond : FiniteDimensional.finrank R M = FiniteDimensional.finrank R M'<GOAL>Nonempty (M ≃ₗ[R] M')
<VAR>R : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>Ring R<VAR>StrongRankCondition R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<VAR>AddCommGroup M'<VAR>Module R M'<VAR>Module.Free R M'<VAR>Module.Finite R M<VAR>Module.Finite R M'<GOAL>Nonempty (M ≃ₗ[R] M') ↔ FiniteDimensional.finrank R M = FiniteDimensional.finrank R M'
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>StrongRankCondition R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<GOAL>Module.rank R M < ℵ₀ ↔ Module.Finite R M
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>StrongRankCondition R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<VAR>h : ¬Module.Finite R M<GOAL>FiniteDimensional.finrank R M = 0
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>StrongRankCondition R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<VAR>h : 0 < FiniteDimensional.finrank R M<GOAL>Module.Finite R M
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>StrongRankCondition R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<VAR>n : ℕ<VAR>hn : FiniteDimensional.finrank R M = n.succ<GOAL>Module.Finite R M
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>StrongRankCondition R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<VAR>W : Type v<VAR>AddCommGroup W<VAR>Module R W<VAR>Module.Free R W<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hVW : Module.rank R M = n • Module.rank R W<GOAL>Module.Finite R M ↔ Module.Finite R W
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>StrongRankCondition R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<VAR>ι : Type u_1<VAR>Unique ι<VAR>h : FiniteDimensional.finrank R M = 1<VAR>v : M<VAR>i : ι<GOAL>((FiniteDimensional.basisUnique ι h).repr v) i = 0 ↔ v = 0
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>m : M<GOAL>(ExteriorAlgebra.ι R) m * (ExteriorAlgebra.ι R) m = 0
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>A : Type u_1<VAR>Semiring A<VAR>Algebra R A<VAR>g : ExteriorAlgebra R M →ₐ[R] A<VAR>m : M<GOAL>g ((ExteriorAlgebra.ι R) m) * g ((ExteriorAlgebra.ι R) m) = 0
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>A : Type u_1<VAR>Semiring A<VAR>Algebra R A<GOAL>∀ (a : ExteriorAlgebra R M →ₐ[R] A), (ExteriorAlgebra.lift R).symm a = ⟨↑((CliffordAlgebra.lift 0).symm a), ⋯⟩
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>A : Type u_1<VAR>Semiring A<VAR>Algebra R A<VAR>f : M →ₗ[R] A<VAR>cond : ∀ (m : M), f m * f m = 0<GOAL>((ExteriorAlgebra.lift R) ⟨f, cond⟩).toLinearMap ∘ₗ ExteriorAlgebra.ι R = f
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>A : Type u_1<VAR>Semiring A<VAR>Algebra R A<VAR>f : M →ₗ[R] A<VAR>cond : ∀ (m : M), f m * f m = 0<VAR>x : M<GOAL>((ExteriorAlgebra.lift R) ⟨f, cond⟩) ((ExteriorAlgebra.ι R) x) = f x
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>A : Type u_1<VAR>Semiring A<VAR>Algebra R A<VAR>f : M →ₗ[R] A<VAR>cond : ∀ (m : M), f m * f m = 0<VAR>g : ExteriorAlgebra R M →ₐ[R] A<GOAL>g.toLinearMap ∘ₗ ExteriorAlgebra.ι R = f ↔ g = (ExteriorAlgebra.lift R) ⟨f, cond⟩
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>A : Type u_1<VAR>Semiring A<VAR>Algebra R A<VAR>g : ExteriorAlgebra R M →ₐ[R] A<GOAL>(ExteriorAlgebra.lift R) ⟨g.toLinearMap ∘ₗ ExteriorAlgebra.ι R, ⋯⟩ = g
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>A : Type u_1<VAR>Semiring A<VAR>Algebra R A<VAR>f g : ExteriorAlgebra R M →ₐ[R] A<VAR>h : f.toLinearMap ∘ₗ ExteriorAlgebra.ι R = g.toLinearMap ∘ₗ ExteriorAlgebra.ι R<GOAL>f = g
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>C : ExteriorAlgebra R M → Prop<VAR>algebraMap : ∀ (r : R), C ((algebraMap R (ExteriorAlgebra R M)) r)<VAR>ι : ∀ (x : M), C ((ExteriorAlgebra.ι R) x)<VAR>mul : ∀ (a b : ExteriorAlgebra R M), C a → C b → C (a * b)<VAR>add : ∀ (a b : ExteriorAlgebra R M), C a → C b → C (a + b)<VAR>a : ExteriorAlgebra R M<GOAL>C a
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<GOAL>Function.LeftInverse ⇑ExteriorAlgebra.algebraMapInv ⇑(algebraMap R (ExteriorAlgebra R M))
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>x y : R<GOAL>(algebraMap R (ExteriorAlgebra R M)) x = (algebraMap R (ExteriorAlgebra R M)) y ↔ x = y
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>x : R<GOAL>(algebraMap R (ExteriorAlgebra R M)) x = 0 ↔ x = 0
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>x : R<GOAL>(algebraMap R (ExteriorAlgebra R M)) x = 1 ↔ x = 1
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>r : R<GOAL>IsUnit ((algebraMap R (ExteriorAlgebra R M)) r) ↔ IsUnit r
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>r : R<GOAL>∀ (x : Invertible ((algebraMap R (ExteriorAlgebra R M)) r)), ⅟r = ⅟(ExteriorAlgebra.algebraMapInv ((algebraMap R (ExteriorAlgebra R M)) r))
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>r : R<GOAL>∀ (x : Invertible r), (⅟((algebraMap R (ExteriorAlgebra R M)) r)).toQuot = Quot.mk (RingQuot.Rel (CliffordAlgebra.Rel 0)) ((algebraMap R (TensorAlgebra R M)) ⅟r)
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>Module Rᵐᵒᵖ M<VAR>IsCentralScalar R M<VAR>x : M<GOAL>ExteriorAlgebra.toTrivSqZeroExt ((ExteriorAlgebra.ι R) x) = TrivSqZeroExt.inr x
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<GOAL>Function.LeftInverse ⇑ExteriorAlgebra.ιInv ⇑(ExteriorAlgebra.ι R)
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>x y : M<GOAL>(ExteriorAlgebra.ι R) x = (ExteriorAlgebra.ι R) y ↔ x = y
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>x : M<GOAL>(ExteriorAlgebra.ι R) x = 0 ↔ x = 0
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>x : M<VAR>r : R<GOAL>(ExteriorAlgebra.ι R) x = (algebraMap R (ExteriorAlgebra R M)) r ↔ x = 0 ∧ r = 0
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>Nontrivial R<VAR>x : M<GOAL>(ExteriorAlgebra.ι R) x ≠ 1
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<GOAL>Disjoint (LinearMap.range (ExteriorAlgebra.ι R)) 1
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>x y : M<GOAL>(ExteriorAlgebra.ι R) x * (ExteriorAlgebra.ι R) y + (ExteriorAlgebra.ι R) y * (ExteriorAlgebra.ι R) x = 0
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>n : ℕ<VAR>f : Fin n → M<VAR>i : Fin n<GOAL>(ExteriorAlgebra.ι R) (f i) * (List.ofFn fun i => (ExteriorAlgebra.ι R) (f i)).prod = 0
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>n : ℕ<VAR>v : Fin n → M<GOAL>(ExteriorAlgebra.ιMulti R n) v = (List.ofFn fun i => (ExteriorAlgebra.ι R) (v i)).prod
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>v : Fin 0 → M<GOAL>(ExteriorAlgebra.ιMulti R 0) v = 1
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>n : ℕ<VAR>v : Fin n.succ → M<GOAL>(ExteriorAlgebra.ιMulti R n.succ) v = (ExteriorAlgebra.ι R) (v 0) * (ExteriorAlgebra.ιMulti R n) (Matrix.vecTail v)
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>n : ℕ<VAR>m : M<GOAL>(ExteriorAlgebra.ιMulti R n.succ).curryLeft m = (LinearMap.mulLeft R ((ExteriorAlgebra.ι R) m)).compAlternatingMap (ExteriorAlgebra.ιMulti R n)
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>n : ℕ<GOAL>Set.range ⇑(ExteriorAlgebra.ιMulti R n) ⊆ ↑(⋀[R]^n M)
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>n : ℕ<GOAL>Submodule.span R (Set.range ⇑(ExteriorAlgebra.ιMulti R n)) = ⋀[R]^n M
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u4<VAR>AddCommGroup N<VAR>Module R N<VAR>f : M →ₗ[R] N<GOAL>(ExteriorAlgebra.map f).toLinearMap ∘ₗ ExteriorAlgebra.ι R = ExteriorAlgebra.ι R ∘ₗ f
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u4<VAR>AddCommGroup N<VAR>Module R N<VAR>f : M →ₗ[R] N<VAR>m : M<GOAL>(ExteriorAlgebra.map f) ((ExteriorAlgebra.ι R) m) = (ExteriorAlgebra.ι R) (f m)
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u4<VAR>AddCommGroup N<VAR>Module R N<VAR>n : ℕ<VAR>f : M →ₗ[R] N<VAR>m : Fin n → M<GOAL>(ExteriorAlgebra.map f) ((ExteriorAlgebra.ιMulti R n) m) = (ExteriorAlgebra.ιMulti R n) (⇑f ∘ m)
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u4<VAR>AddCommGroup N<VAR>Module R N<VAR>n : ℕ<VAR>f : M →ₗ[R] N<GOAL>(ExteriorAlgebra.map f).toLinearMap.compAlternatingMap (ExteriorAlgebra.ιMulti R n) = (ExteriorAlgebra.ιMulti R n).compLinearMap f
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<GOAL>ExteriorAlgebra.map LinearMap.id = AlgHom.id R (ExteriorAlgebra R M)
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u4<VAR>N' : Type u5<VAR>AddCommGroup N<VAR>Module R N<VAR>AddCommGroup N'<VAR>Module R N'<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] N'<GOAL>(ExteriorAlgebra.map g).comp (ExteriorAlgebra.map f) = ExteriorAlgebra.map (g ∘ₗ f)
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u4<VAR>AddCommGroup N<VAR>Module R N<VAR>f : M →ₗ[R] N<GOAL>Submodule.map (ExteriorAlgebra.map f).toLinearMap (LinearMap.range (ExteriorAlgebra.ι R)) = Submodule.map (ExteriorAlgebra.ι R) (LinearMap.range f)
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u4<VAR>AddCommGroup N<VAR>Module R N<VAR>Module Rᵐᵒᵖ M<VAR>IsCentralScalar R M<VAR>Module Rᵐᵒᵖ N<VAR>IsCentralScalar R N<VAR>f : M →ₗ[R] N<GOAL>ExteriorAlgebra.toTrivSqZeroExt.comp (ExteriorAlgebra.map f) = (TrivSqZeroExt.map f).comp ExteriorAlgebra.toTrivSqZeroExt
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u4<VAR>AddCommGroup N<VAR>Module R N<VAR>f : M →ₗ[R] N<GOAL>ExteriorAlgebra.ιInv ∘ₗ (ExteriorAlgebra.map f).toLinearMap = f ∘ₗ ExteriorAlgebra.ιInv
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u4<VAR>AddCommGroup N<VAR>Module R N<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] M<GOAL>Function.LeftInverse ⇑(ExteriorAlgebra.map g) ⇑(ExteriorAlgebra.map f) ↔ Function.LeftInverse ⇑g ⇑f
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u4<VAR>AddCommGroup N<VAR>Module R N<VAR>f : M →ₗ[R] N<VAR>hf : ∃ g, g ∘ₗ f = LinearMap.id<GOAL>Function.Injective ⇑(ExteriorAlgebra.map f)
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u4<VAR>AddCommGroup N<VAR>Module R N<VAR>f : M →ₗ[R] N<GOAL>Function.Surjective ⇑(ExteriorAlgebra.map f) ↔ Function.Surjective ⇑f
<VAR>K : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>Field K<VAR>AddCommGroup E<VAR>Module K E<VAR>AddCommGroup F<VAR>Module K F<VAR>f : E →ₗ[K] F<VAR>hf : LinearMap.ker f = ⊥<GOAL>Function.Injective ⇑(ExteriorAlgebra.map f)
<VAR>R : Type u1<VAR>CommRing R<VAR>M : Type u2<VAR>AddCommGroup M<VAR>Module R M<VAR>m : M<GOAL>TensorAlgebra.toExterior ((TensorAlgebra.ι R) m) = (ExteriorAlgebra.ι R) m
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type w<VAR>ι' : Type w'<VAR>InvariantBasisNumber R<VAR>v : Basis ι R M<VAR>v' : Basis ι' R M<GOAL>Cardinal.lift.{w', w} #ι = Cardinal.lift.{w, w'} #ι'
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type w<VAR>InvariantBasisNumber R<VAR>ι' : Type w<VAR>v : Basis ι R M<VAR>v' : Basis ι' R M<GOAL>#ι = #ι'
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>RankCondition R<VAR>ι : Type u_1<VAR>Fintype ι<VAR>b : Basis ι R M<VAR>w : Set M<VAR>Fintype ↑w<VAR>s : Submodule.span R w = ⊤<GOAL>Fintype.card ι ≤ Fintype.card ↑w
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>RankCondition R<VAR>ι : Type u_1<VAR>b : Basis ι R M<VAR>w : Set M<VAR>Fintype ↑w<VAR>s : Submodule.span R w = ⊤<GOAL>#ι ≤ ↑(Fintype.card ↑w)
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type w<VAR>RankCondition R<VAR>J : Set M<VAR>v : Basis ι R M<VAR>hJ : Submodule.span R J = ⊤<GOAL>#↑(Set.range ⇑v) ≤ #↑J
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>ι : Type u_1<VAR>Fintype ι<VAR>v : ι → M<VAR>i : LinearIndependent R v<VAR>w : Set M<VAR>Fintype ↑w<VAR>s : Set.range v ≤ ↑(Submodule.span R w)<GOAL>Fintype.card ι ≤ Fintype.card ↑w
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>ι : Type u_1<VAR>v : ι → M<VAR>i : LinearIndependent R v<VAR>w : Set M<VAR>Finite ↑w<VAR>s : Set.range v ≤ ↑(Submodule.span R w)<GOAL>Finite ι
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>ι : Type u_1<VAR>v : ι → M<VAR>i : LinearIndependent R v<VAR>w : Set M<VAR>Fintype ↑w<VAR>s : Set.range v ≤ ↑(Submodule.span R w)<GOAL>#ι ≤ ↑(Fintype.card ↑w)
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>ι : Type u_1<VAR>v : ι → M<VAR>i : LinearIndependent R v<VAR>w : Set M<VAR>Fintype ↑w<VAR>s : Submodule.span R w = ⊤<GOAL>#ι ≤ ↑(Fintype.card ↑w)
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>ι : Type u_1<VAR>v : ι → M<VAR>i : LinearIndependent R v<VAR>w : Finset M<VAR>s : Submodule.span R ↑w = ⊤<GOAL>#ι ≤ ↑w.card
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>ι : Type w<VAR>b : Basis ι R M<VAR>Infinite ι<VAR>κ : Type w<VAR>v : κ → M<VAR>i : LinearIndependent R v<GOAL>#κ ≤ #ι
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>ι : Type w<VAR>b : Basis ι R M<VAR>κ : Type w<VAR>v : κ → M<VAR>i : LinearIndependent R v<GOAL>#κ ≤ #ι
<VAR>R : Type u_1<VAR>Ring R<VAR>StrongRankCondition R<VAR>n : ℕ<VAR>m : ℕ<VAR>v : Fin m → Fin n → R<GOAL>LinearIndependent R v → m ≤ n
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>ι : Type w<VAR>b : Basis ι R M<VAR>Infinite ι<VAR>κ : Type w<VAR>v : κ → M<VAR>i : LinearIndependent R v<VAR>m : i.Maximal<GOAL>#κ = #ι
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>ι : Type v<VAR>v : Basis ι R M<GOAL>#ι = Module.rank R M
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type w<VAR>StrongRankCondition R<VAR>v : Basis ι R M<GOAL>#↑(Set.range ⇑v) = Module.rank R M
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>ι : Type w<VAR>Fintype ι<VAR>h : Basis ι R M<GOAL>Module.rank R M = ↑(Fintype.card ι)
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>ι : Type u_1<VAR>Fintype ι<VAR>b : Basis ι R M<VAR>ι' : Type u_2<VAR>Fintype ι'<VAR>v : ι' → M<VAR>hv : LinearIndependent R v<GOAL>Fintype.card ι' ≤ Fintype.card ι
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type w<VAR>ι' : Type w'<VAR>StrongRankCondition R<VAR>N : Submodule R M<VAR>Fintype ι<VAR>b : Basis ι R M<VAR>Fintype ι'<VAR>b' : Basis ι' R ↥N<GOAL>Fintype.card ι' ≤ Fintype.card ι