ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>S : Set (Projectivization K V)<VAR>W : Projectivization.Subspace K V<GOAL>Projectivization.Subspace.span S ≤ W ↔ S ⊆ ↑W
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<GOAL>Monotone Projectivization.Subspace.span
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>S T U : Set (Projectivization K V)<VAR>hST : S ⊆ ↑(Projectivization.Subspace.span T)<VAR>hTU : T ⊆ ↑(Projectivization.Subspace.span U)<GOAL>S ⊆ ↑(Projectivization.Subspace.span U)
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>S T : Set (Projectivization K V)<GOAL>Projectivization.Subspace.span (S ∪ T) = Projectivization.Subspace.span S ⊔ Projectivization.Subspace.span T
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>ι : Sort u_3<VAR>s : ι → Set (Projectivization K V)<GOAL>Projectivization.Subspace.span (⋃ i, s i) = ⨆ i, Projectivization.Subspace.span (s i)
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>S : Set (Projectivization K V)<VAR>W : Projectivization.Subspace K V<GOAL>W ⊔ Projectivization.Subspace.span S = Projectivization.Subspace.span (↑W ∪ S)
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>S : Set (Projectivization K V)<VAR>W : Projectivization.Subspace K V<GOAL>Projectivization.Subspace.span S ⊔ W = Projectivization.Subspace.span (S ∪ ↑W)
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>S : Set (Projectivization K V)<VAR>u : Projectivization K V<GOAL>u ∈ Projectivization.Subspace.span S ↔ ∀ (W : Projectivization.Subspace K V), S ⊆ ↑W → u ∈ W
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>S : Set (Projectivization K V)<GOAL>Projectivization.Subspace.span S = sInf {W | S ⊆ ↑W}
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>S : Set (Projectivization K V)<VAR>W : Projectivization.Subspace K V<VAR>hS : S ⊆ ↑W<VAR>hW : W ≤ Projectivization.Subspace.span S<GOAL>Projectivization.Subspace.span S = W
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>S T : Set (Projectivization K V)<GOAL>Projectivization.Subspace.span S = Projectivization.Subspace.span T ↔ S ⊆ ↑(Projectivization.Subspace.span T) ∧ T ⊆ ↑(Projectivization.Subspace.span S)
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>M' : Submodule R M<VAR>ι₁ : Type u_2<VAR>ι₂ : Type u_3<VAR>f : ι₁ → ↥M'<VAR>hf : LinearIndependent R f<VAR>g : ι₂ → M<VAR>hg : LinearIndependent R (Submodule.Quotient.mk ∘ g)<GOAL>LinearIndependent R (Sum.elim (fun x => ↑(f x)) g)
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>M' : Submodule R M<VAR>s : Set M<VAR>hs : s ⊆ ↑M'<VAR>hs' : LinearIndependent (ι := ↑s) R Subtype.val<VAR>t : Set M<VAR>ht : LinearIndependent (ι := ↑t) R (Submodule.Quotient.mk ∘ Subtype.val)<GOAL>LinearIndependent (ι := ↑(s ∪ t)) R Subtype.val
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>Nontrivial R<VAR>M' : Submodule R M<GOAL>Module.rank R (M ⧸ M') + Module.rank R ↥M' ≤ Module.rank R M
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<GOAL>Module.rank R (M ⧸ p) ≤ Module.rank R M
<VAR>R : Type u_2<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>M' : Submodule R M<VAR>hN : M' ≤ Submodule.torsion R M<GOAL>Module.rank R (M ⧸ M') = Module.rank R M
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<GOAL>Module.rank R (ULift.{w, v} M) = Cardinal.lift.{w, v} (Module.rank R M)
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<GOAL>FiniteDimensional.finrank R (ULift.{u_2, v} M) = FiniteDimensional.finrank R M
<VAR>R : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>Ring R<VAR>AddCommGroup M<VAR>AddCommGroup M'<VAR>Module R M<VAR>Module R M'<VAR>Nontrivial R<GOAL>Cardinal.lift.{v', v} (Module.rank R M) + Cardinal.lift.{v, v'} (Module.rank R M') ≤ Module.rank R (M × M')
<VAR>R : Type u<VAR>M : Type v<VAR>M₁ : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>AddCommGroup M₁<VAR>Module R M<VAR>Module R M₁<VAR>Nontrivial R<GOAL>Module.rank R M + Module.rank R M₁ ≤ Module.rank R (M × M₁)
<VAR>R : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>Ring R<VAR>AddCommGroup M<VAR>AddCommGroup M'<VAR>Module R M<VAR>Module R M'<VAR>StrongRankCondition R<VAR>Module.Free R M<VAR>Module.Free R M'<GOAL>Module.rank R (M × 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>AddCommGroup M<VAR>AddCommGroup M₁<VAR>Module R M<VAR>Module R M₁<VAR>StrongRankCondition R<VAR>Module.Free R M<VAR>Module.Free R M₁<GOAL>Module.rank R (M × 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>AddCommGroup M<VAR>AddCommGroup M'<VAR>Module R M<VAR>Module R M'<VAR>StrongRankCondition R<VAR>Module.Free R M<VAR>Module.Free R M'<VAR>Module.Finite R M<VAR>Module.Finite R M'<GOAL>FiniteDimensional.finrank R (M × M') = FiniteDimensional.finrank R M + FiniteDimensional.finrank R M'
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>Module.Free R M<VAR>ι : Type w<GOAL>Module.rank R (ι →₀ M) = Cardinal.lift.{v, w} #ι * Cardinal.lift.{w, 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>Module.Free R M<VAR>ι : Type v<GOAL>Module.rank R (ι →₀ M) = #ι * Module.rank R M
<VAR>R : Type u<VAR>Ring R<VAR>StrongRankCondition R<VAR>ι : Type w<GOAL>Module.rank R (ι →₀ R) = Cardinal.lift.{u, w} #ι
<VAR>R : Type u<VAR>Ring R<VAR>StrongRankCondition R<VAR>ι : Type u<GOAL>Module.rank R (ι →₀ R) = #ι
<VAR>R : Type u<VAR>Ring R<VAR>StrongRankCondition R<VAR>ι : Type v<VAR>M : ι → Type w<VAR>(i : ι) → AddCommGroup (M i)<VAR>(i : ι) → Module R (M i)<VAR>∀ (i : ι), Module.Free R (M i)<GOAL>Module.rank R (⨁ (i : ι), M i) = Cardinal.sum fun i => Module.rank R (M i)
<VAR>R : Type u<VAR>Ring R<VAR>StrongRankCondition R<VAR>m : Type v<VAR>n : Type w<VAR>Finite m<VAR>Finite n<GOAL>Module.rank R (Matrix m n R) = Cardinal.lift.{max v w u, v} #m * Cardinal.lift.{max v w u, w} #n
<VAR>R : Type u<VAR>Ring R<VAR>StrongRankCondition R<VAR>m n : Type v<VAR>Finite m<VAR>Finite n<GOAL>Module.rank R (Matrix m n R) = Cardinal.lift.{u, v} (#m * #n)
<VAR>R : Type u<VAR>Ring R<VAR>StrongRankCondition R<VAR>m n : Type u<VAR>Finite m<VAR>Finite n<GOAL>Module.rank R (Matrix m n R) = #m * #n
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>Module.Free R M<VAR>ι : Type v<VAR>Fintype ι<GOAL>FiniteDimensional.finrank R (ι →₀ M) = Fintype.card ι * FiniteDimensional.finrank R M
<VAR>R : Type u<VAR>Ring R<VAR>StrongRankCondition R<VAR>ι : Type v<VAR>Fintype ι<GOAL>FiniteDimensional.finrank R (ι →₀ R) = Fintype.card ι
<VAR>R : Type u<VAR>Ring R<VAR>StrongRankCondition R<VAR>ι : Type v<VAR>Fintype ι<VAR>M : ι → Type w<VAR>(i : ι) → AddCommGroup (M i)<VAR>(i : ι) → Module R (M i)<VAR>∀ (i : ι), Module.Free R (M i)<VAR>∀ (i : ι), Module.Finite R (M i)<GOAL>FiniteDimensional.finrank R (⨁ (i : ι), M i) = ∑ i : ι, FiniteDimensional.finrank R (M i)
<VAR>R : Type u<VAR>Ring R<VAR>StrongRankCondition R<VAR>m : Type u_2<VAR>n : Type u_3<VAR>Fintype m<VAR>Fintype n<GOAL>FiniteDimensional.finrank R (Matrix m n R) = Fintype.card m * Fintype.card n
<VAR>R : Type u<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>Ring R<VAR>StrongRankCondition R<VAR>(i : η) → AddCommGroup (φ i)<VAR>(i : η) → Module R (φ i)<VAR>∀ (i : η), Module.Free R (φ i)<VAR>Finite η<GOAL>Module.rank R ((i : η) → φ i) = Cardinal.sum fun i => Module.rank R (φ i)
<VAR>R : Type u<VAR>Ring R<VAR>StrongRankCondition R<VAR>ι : Type v<VAR>Fintype ι<GOAL>FiniteDimensional.finrank R (ι → R) = Fintype.card ι
<VAR>R : Type u<VAR>Ring R<VAR>StrongRankCondition R<VAR>ι : Type v<VAR>Fintype ι<VAR>M : ι → Type w<VAR>(i : ι) → AddCommGroup (M i)<VAR>(i : ι) → Module R (M i)<VAR>∀ (i : ι), Module.Free R (M i)<VAR>∀ (i : ι), Module.Finite R (M i)<GOAL>FiniteDimensional.finrank R ((i : ι) → M i) = ∑ i : ι, FiniteDimensional.finrank R (M i)
<VAR>R : Type u<VAR>Ring R<VAR>StrongRankCondition R<VAR>M η : Type u<VAR>Fintype η<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<GOAL>Module.rank R (η → M) = ↑(Fintype.card η) * Module.rank R M
<VAR>R : Type u<VAR>M : Type v<VAR>η : Type u₁'<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>Module.Free R M<VAR>Fintype η<GOAL>Module.rank R (η → M) = ↑(Fintype.card η) * Cardinal.lift.{u₁', v} (Module.rank R M)
<VAR>R : Type u<VAR>η : Type u₁'<VAR>Ring R<VAR>StrongRankCondition R<VAR>Fintype η<GOAL>Module.rank R (η → R) = ↑(Fintype.card η)
<VAR>R : Type u<VAR>Ring R<VAR>StrongRankCondition R<VAR>n : ℕ<GOAL>Module.rank R (Fin n → R) = ↑n
<VAR>R : Type u<VAR>η : Type u₁'<VAR>Ring R<VAR>StrongRankCondition R<VAR>Fintype η<GOAL>FiniteDimensional.finrank R (η → R) = Fintype.card η
<VAR>R : Type u<VAR>Ring R<VAR>StrongRankCondition R<VAR>n : ℕ<GOAL>FiniteDimensional.finrank R (Fin n → R) = n
<VAR>R S : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>Ring R<VAR>CommRing S<VAR>AddCommGroup M<VAR>AddCommGroup M'<VAR>StrongRankCondition R<VAR>StrongRankCondition S<VAR>Module S M<VAR>Module S M'<VAR>Module.Free S M'<VAR>Algebra S R<VAR>Module R M<VAR>IsScalarTower S R M<VAR>Module.Free R M<GOAL>Module.rank R (TensorProduct S M M') = Cardinal.lift.{v', v} (Module.rank R M) * Cardinal.lift.{v, v'} (Module.rank S M')
<VAR>R S : Type u<VAR>M M₁ : Type v<VAR>Ring R<VAR>CommRing S<VAR>AddCommGroup M<VAR>AddCommGroup M₁<VAR>StrongRankCondition R<VAR>StrongRankCondition S<VAR>Module S M<VAR>Module S M₁<VAR>Module.Free S M₁<VAR>Algebra S R<VAR>Module R M<VAR>IsScalarTower S R M<VAR>Module.Free R M<GOAL>Module.rank R (TensorProduct S M M₁) = Module.rank R M * Module.rank S M₁
<VAR>R S : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>Ring R<VAR>CommRing S<VAR>AddCommGroup M<VAR>AddCommGroup M'<VAR>StrongRankCondition R<VAR>StrongRankCondition S<VAR>Module S M<VAR>Module S M'<VAR>Module.Free S M'<VAR>Algebra S R<VAR>Module R M<VAR>IsScalarTower S R M<VAR>Module.Free R M<GOAL>FiniteDimensional.finrank R (TensorProduct S M M') = FiniteDimensional.finrank R M * FiniteDimensional.finrank S M'
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>s t : Submodule R M<VAR>le : s ≤ t<VAR>lt : FiniteDimensional.finrank R ↥s < FiniteDimensional.finrank R ↥t<GOAL>s < t
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>s : Submodule R M<VAR>lt : FiniteDimensional.finrank R ↥s < FiniteDimensional.finrank R M<GOAL>s < ⊤
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>Module.Finite R M<VAR>s : Submodule R M<GOAL>FiniteDimensional.finrank R ↥s ≤ FiniteDimensional.finrank R M
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>Module.Finite R M<VAR>s : Submodule R M<GOAL>FiniteDimensional.finrank R (M ⧸ s) ≤ FiniteDimensional.finrank R M
<VAR>R : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>Ring R<VAR>AddCommGroup M<VAR>AddCommGroup M'<VAR>Module R M<VAR>Module R M'<VAR>StrongRankCondition R<VAR>f : M →ₗ[R] M'<VAR>p : Submodule R M<VAR>Module.Finite R ↥p<GOAL>FiniteDimensional.finrank R ↥(Submodule.map f p) ≤ FiniteDimensional.finrank R ↥p
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>s t : Submodule R M<VAR>Module.Finite R ↥t<VAR>hst : s ≤ t<GOAL>FiniteDimensional.finrank R ↥s ≤ FiniteDimensional.finrank R ↥t
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>s : Set M<GOAL>Module.rank R ↥(Submodule.span R s) ≤ #↑s
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>s : Finset M<GOAL>Module.rank R ↥(Submodule.span R ↑s) ≤ ↑s.card
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>s : Finset M<GOAL>Module.rank R ↥(Submodule.span R ↑s) < ℵ₀
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>s : Set M<VAR>Fintype ↑s<GOAL>FiniteDimensional.finrank R ↥(Submodule.span R s) ≤ s.toFinset.card
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>s : Finset M<GOAL>Set.finrank R ↑s ≤ s.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_2<VAR>Fintype ι<VAR>b : ι → M<GOAL>Set.finrank R (Set.range b) ≤ Fintype.card ι
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>Nontrivial R<VAR>ι : Type u_2<VAR>Fintype ι<VAR>b : ι → M<VAR>hb : LinearIndependent R b<GOAL>FiniteDimensional.finrank R ↥(Submodule.span R (Set.range b)) = Fintype.card ι
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>s : Set M<VAR>Fintype ↑s<VAR>hs : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val<GOAL>FiniteDimensional.finrank R ↥(Submodule.span R s) = s.toFinset.card
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>s : Finset M<VAR>hs : LinearIndependent R Subtype.val<GOAL>FiniteDimensional.finrank R ↥(Submodule.span R ↑s) = s.card
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>s : Set M<VAR>Fintype ↑s<VAR>t : Submodule R M<VAR>subset : s ⊆ ↑t<VAR>card_lt : s.toFinset.card < FiniteDimensional.finrank R ↥t<GOAL>Submodule.span R s < t
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>s : Set M<VAR>Fintype ↑s<VAR>card_lt : s.toFinset.card < FiniteDimensional.finrank R M<GOAL>Submodule.span R s < ⊤
<VAR>F : Type u_2<VAR>E : Type u_3<VAR>CommRing F<VAR>Ring E<VAR>Algebra F E<VAR>S : Subalgebra F E<GOAL>Module.rank F ↥(Subalgebra.toSubmodule S) = Module.rank F ↥S
<VAR>F : Type u_2<VAR>E : Type u_3<VAR>CommRing F<VAR>Ring E<VAR>Algebra F E<VAR>S : Subalgebra F E<GOAL>FiniteDimensional.finrank F ↥(Subalgebra.toSubmodule S) = FiniteDimensional.finrank F ↥S
<VAR>F : Type u_2<VAR>E : Type u_3<VAR>CommRing F<VAR>Ring E<VAR>Algebra F E<GOAL>Module.rank F ↥⊤ = Module.rank F ↥⊤
<VAR>F : Type u_2<VAR>E : Type u_3<VAR>CommRing F<VAR>Ring E<VAR>Algebra F E<GOAL>FiniteDimensional.finrank F ↥⊤ = FiniteDimensional.finrank F ↥⊤
<VAR>F : Type u_2<VAR>E : Type u_3<VAR>CommRing F<VAR>Ring E<VAR>Algebra F E<GOAL>Module.rank F ↥⊤ = Module.rank F E
<VAR>F : Type u_2<VAR>E : Type u_3<VAR>CommRing F<VAR>Ring E<VAR>Algebra F E<VAR>StrongRankCondition F<VAR>NoZeroSMulDivisors F E<VAR>Nontrivial E<GOAL>Module.rank F ↥⊥ = 1
<VAR>F : Type u_2<VAR>E : Type u_3<VAR>CommRing F<VAR>Ring E<VAR>Algebra F E<VAR>StrongRankCondition F<VAR>NoZeroSMulDivisors F E<VAR>Nontrivial E<GOAL>FiniteDimensional.finrank F ↥⊥ = 1
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>v : { v // v ≠ 0 }<GOAL>Projectivization.mk' K v = Projectivization.mk K ↑v ⋯
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>v : Projectivization K V<GOAL>v.rep ≠ 0
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>v : Projectivization K V<GOAL>Projectivization.mk K v.rep ⋯ = v
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>v w : V<VAR>hv : v ≠ 0<VAR>hw : w ≠ 0<GOAL>Projectivization.mk K v hv = Projectivization.mk K w hw ↔ ∃ a, a • w = v
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>v : V<VAR>hv : v ≠ 0<GOAL>∃ a, a • v = (Projectivization.mk K v hv).rep
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>P : Projectivization K V → Prop<VAR>h : ∀ (v : V) (h : v ≠ 0), P (Projectivization.mk K v h)<VAR>p : Projectivization K V<GOAL>P p
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>v : V<VAR>hv : v ≠ 0<GOAL>(Projectivization.mk K v hv).submodule = Submodule.span K {v}
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>v : Projectivization K V<GOAL>v.submodule = Submodule.span K {v.rep}
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>v : Projectivization K V<GOAL>FiniteDimensional.finrank K ↥v.submodule = 1
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<GOAL>Function.Injective Projectivization.submodule
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>H : Submodule K V<VAR>h : FiniteDimensional.finrank K ↥H = 1<GOAL>(Projectivization.mk'' H h).submodule = H
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>v : Projectivization K V<GOAL>Projectivization.mk'' v.submodule ⋯ = v
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>L : Type u_3<VAR>W : Type u_4<VAR>DivisionRing L<VAR>AddCommGroup W<VAR>Module L W<VAR>σ : K →+* L<VAR>f : V →ₛₗ[σ] W<VAR>hf : Function.Injective ⇑f<VAR>v : V<VAR>hv : v ≠ 0<GOAL>Projectivization.map f hf (Projectivization.mk K v hv) = Projectivization.mk L (f v) ⋯
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>L : Type u_3<VAR>W : Type u_4<VAR>DivisionRing L<VAR>AddCommGroup W<VAR>Module L W<VAR>σ : K →+* L<VAR>τ : L →+* K<VAR>RingHomInvPair σ τ<VAR>f : V →ₛₗ[σ] W<VAR>hf : Function.Injective ⇑f<GOAL>Function.Injective (Projectivization.map f hf)
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<GOAL>Projectivization.map LinearMap.id ⋯ = id
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>L : Type u_3<VAR>W : Type u_4<VAR>DivisionRing L<VAR>AddCommGroup W<VAR>Module L W<VAR>F : Type u_5<VAR>U : Type u_6<VAR>Field F<VAR>AddCommGroup U<VAR>Module F U<VAR>σ : K →+* L<VAR>τ : L →+* F<VAR>γ : K →+* F<VAR>RingHomCompTriple σ τ γ<VAR>f : V →ₛₗ[σ] W<VAR>hf : Function.Injective ⇑f<VAR>g : W →ₛₗ[τ] U<VAR>hg : Function.Injective ⇑g<GOAL>Projectivization.map (g.comp f) ⋯ = Projectivization.map g hg ∘ Projectivization.map f hf
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>f g : Module.End R M<VAR>μ : R<VAR>k : ℕ<VAR>m : M<VAR>hm : m ∈ (f.genEigenspace μ) k<VAR>hfg : Commute f g<VAR>hss : g.IsSemisimple<VAR>hnil : IsNilpotent (f - g)<GOAL>g m = μ • m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>f : Module.End R M<VAR>hf : f.IsSemisimple<VAR>μ : R<VAR>k : ℕ<VAR>hk : 0 < k<GOAL>(f.genEigenspace μ) k = f.eigenspace μ
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>f : Module.End R M<VAR>hf : f.IsSemisimple<VAR>μ : R<GOAL>f.maxGenEigenspace μ = f.eigenspace μ
<VAR>R : Type u_3<VAR>CommSemiring R<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>Module R M<GOAL>TensorAlgebra.ι R = { toFun := fun m => (RingQuot.mkAlgHom R (TensorAlgebra.Rel R M)) (FreeAlgebra.ι R m), map_add' := ⋯, map_smul' := ⋯ }
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>m : M<GOAL>(RingQuot.mkAlgHom R (TensorAlgebra.Rel R M)) (FreeAlgebra.ι R m) = (TensorAlgebra.ι R) m
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>A : Type u_3<VAR>Semiring A<VAR>Algebra R A<VAR>F : TensorAlgebra R M →ₐ[R] A<GOAL>(TensorAlgebra.lift R).symm F = F.toLinearMap ∘ₗ TensorAlgebra.ι R
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>A : Type u_3<VAR>Semiring A<VAR>Algebra R A<VAR>f : M →ₗ[R] A<GOAL>((TensorAlgebra.lift R) f).toLinearMap ∘ₗ TensorAlgebra.ι R = f
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>A : Type u_3<VAR>Semiring A<VAR>Algebra R A<VAR>f : M →ₗ[R] A<VAR>x : M<GOAL>((TensorAlgebra.lift R) f) ((TensorAlgebra.ι R) x) = f x
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>A : Type u_3<VAR>Semiring A<VAR>Algebra R A<VAR>f : M →ₗ[R] A<VAR>g : TensorAlgebra R M →ₐ[R] A<GOAL>g.toLinearMap ∘ₗ TensorAlgebra.ι R = f ↔ g = (TensorAlgebra.lift R) f
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>A : Type u_3<VAR>Semiring A<VAR>Algebra R A<VAR>g : TensorAlgebra R M →ₐ[R] A<GOAL>(TensorAlgebra.lift R) (g.toLinearMap ∘ₗ TensorAlgebra.ι R) = g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>A : Type u_3<VAR>Semiring A<VAR>Algebra R A<VAR>f g : TensorAlgebra R M →ₐ[R] A<VAR>w : f.toLinearMap ∘ₗ TensorAlgebra.ι R = g.toLinearMap ∘ₗ TensorAlgebra.ι R<GOAL>f = g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>C : TensorAlgebra R M → Prop<VAR>algebraMap : ∀ (r : R), C ((algebraMap R (TensorAlgebra R M)) r)<VAR>ι : ∀ (x : M), C ((TensorAlgebra.ι R) x)<VAR>mul : ∀ (a b : TensorAlgebra R M), C a → C b → C (a * b)<VAR>add : ∀ (a b : TensorAlgebra R M), C a → C b → C (a + b)<VAR>a : TensorAlgebra R M<GOAL>C a
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<GOAL>Function.LeftInverse ⇑TensorAlgebra.algebraMapInv ⇑(algebraMap R (TensorAlgebra R M))
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>x y : R<GOAL>(algebraMap R (TensorAlgebra R M)) x = (algebraMap R (TensorAlgebra R M)) y ↔ x = y
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : R<GOAL>(algebraMap R (TensorAlgebra R M)) x = 0 ↔ x = 0
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : R<GOAL>(algebraMap R (TensorAlgebra R M)) x = 1 ↔ x = 1
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : M<VAR>Module Rᵐᵒᵖ M<VAR>IsCentralScalar R M<GOAL>TensorAlgebra.toTrivSqZeroExt ((TensorAlgebra.ι R) x) = TrivSqZeroExt.inr x
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<GOAL>Function.LeftInverse ⇑TensorAlgebra.ιInv ⇑(TensorAlgebra.ι R)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>x y : M<GOAL>(TensorAlgebra.ι R) x = (TensorAlgebra.ι R) y ↔ x = y
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : M<GOAL>(TensorAlgebra.ι R) x = 0 ↔ x = 0
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : M<VAR>r : R<GOAL>(TensorAlgebra.ι R) x = (algebraMap R (TensorAlgebra R M)) r ↔ x = 0 ∧ r = 0
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>Nontrivial R<VAR>x : M<GOAL>(TensorAlgebra.ι R) x ≠ 1
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<GOAL>Disjoint (LinearMap.range (TensorAlgebra.ι R)) 1
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>n : ℕ<VAR>x : Fin n → M<GOAL>(TensorAlgebra.tprod R M n) x = (List.ofFn fun i => (TensorAlgebra.ι R) (x i)).prod
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>m : M<GOAL>FreeAlgebra.toTensor (FreeAlgebra.ι R m) = (TensorAlgebra.ι R) m
<VAR>ι₁ : Type u_1<VAR>ι₂ : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>S : Type u_5<VAR>S₂ : Type u_6<VAR>M : Type u_7<VAR>N : Type u_8<VAR>P : Type u_9<VAR>Semiring R<VAR>Semiring S<VAR>Semiring R₂<VAR>Semiring S₂<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module S N<VAR>Module R₂ P<VAR>Module S₂ P<VAR>SMulCommClass S₂ R₂ P<VAR>ρ₁₂ : R →+* R₂<VAR>σ₁₂ : S →+* S₂<VAR>b₁ : Basis ι₁ R M<VAR>b₂ : Basis ι₂ S N<VAR>B B' : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P<VAR>h : ∀ (i : ι₁) (j : ι₂), (B (b₁ i)) (b₂ j) = (B' (b₁ i)) (b₂ j)<GOAL>B = B'