ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>p : PerfectPairing R M N<VAR>f : Module.Dual R N<VAR>x : N<GOAL>(p (p.toDualLeft.symm f)) x = f x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>p : PerfectPairing R M N<VAR>a : N<GOAL>p.toDualRight a = p.flip a
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>p : PerfectPairing R M N<VAR>x : M<VAR>f : Module.Dual R M<GOAL>(p x) (p.toDualRight.symm f) = f x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>p : PerfectPairing R M N<VAR>x : M<VAR>f : Module.Dual R M<GOAL>(p.toDualLeft x) (p.toDualRight.symm f) = f x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>p : PerfectPairing R M N<VAR>x : M<GOAL>p.toDualRight.symm.dualMap (p.toDualLeft x) = (Module.Dual.eval R M) x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>p : PerfectPairing R M N<GOAL>↑p.toDualRight.symm.dualMap ∘ₗ ↑p.toDualLeft = Module.Dual.eval R M
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>p : PerfectPairing R M N<GOAL>Function.Bijective fun x => p.toDualRight.symm.dualMap (p.toDualLeft x)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>p : PerfectPairing R M N<GOAL>Module.IsReflexive R M
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>p : PerfectPairing R M N<GOAL>Module.IsReflexive R N
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.IsReflexive R M<GOAL>IsReflexive.toPerfectPairingDual.toLin = LinearMap.id
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>Module.IsReflexive R M<VAR>e : N ≃ₗ[R] Module.Dual R M<GOAL>↑e.flip = (↑e).flip
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>Module.IsReflexive R M<VAR>e : N ≃ₗ[R] Module.Dual R M<VAR>m : M<VAR>n : N<GOAL>(e.flip m) n = (e n) m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>Module.IsReflexive R M<VAR>e : N ≃ₗ[R] Module.Dual R M<GOAL>e.flip.symm = e.symm.dualMap ≪≫ₗ (Module.evalEquiv R M).symm
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>Module.IsReflexive R M<VAR>e : N ≃ₗ[R] Module.Dual R M<GOAL>↑(e ≪≫ₗ e.flip.symm.dualMap) = Module.Dual.eval R N
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>Module.IsReflexive R M<VAR>e : N ≃ₗ[R] Module.Dual R M<GOAL>Module.IsReflexive R N
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>Module.IsReflexive R M<VAR>e : N ≃ₗ[R] Module.Dual R M<VAR>h : Module.IsReflexive R N := ⋯<GOAL>e.flip.flip = e
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>Module.IsReflexive R M<VAR>e : N ≃ₗ[R] Module.Dual R M<GOAL>e.toPerfectPairing.toLin = ↑e
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>Module.IsReflexive R M<VAR>e : N ≃ₗ[R] Module.Dual R M<VAR>p : Submodule R M<GOAL>(Submodule.map e.flip p).dualCoannihilator = Submodule.map e.symm p.dualAnnihilator
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>Module.IsReflexive R M<VAR>e : N ≃ₗ[R] Module.Dual R M<VAR>p : Submodule R N<GOAL>Submodule.map e.flip.symm p.dualAnnihilator = (Submodule.map e p).dualCoannihilator
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>Module.IsReflexive R M<VAR>e : N ≃ₗ[R] Module.Dual R M<VAR>p : Submodule R (Module.Dual R M)<GOAL>Submodule.map e.flip p.dualCoannihilator = (Submodule.map e.symm p).dualAnnihilator
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>Module.IsReflexive R M<VAR>e : N ≃ₗ[R] Module.Dual R M<VAR>p : Submodule R (Module.Dual R N)<GOAL>(Submodule.map e.flip.symm p).dualAnnihilator = Submodule.map e p.dualCoannihilator
<VAR>R : Type u<VAR>CommRing R<VAR>n : Type v<VAR>DecidableEq n<VAR>Fintype n<VAR>M : Matrix n n R<VAR>Nontrivial R<VAR>i j : n<GOAL>(M.charmatrix i j).natDegree = if i = j then 1 else 0
<VAR>R : Type u<VAR>CommRing R<VAR>n : Type v<VAR>DecidableEq n<VAR>Fintype n<VAR>M : Matrix n n R<VAR>i j : n<GOAL>(M.charmatrix i j).natDegree ≤ if i = j then 1 else 0
<VAR>R : Type u<VAR>CommRing R<VAR>n : Type v<VAR>DecidableEq n<VAR>Fintype n<VAR>M : Matrix n n R<GOAL>(M.charpoly - ∏ i : n, (Polynomial.X - Polynomial.C (M i i))).degree < ↑(Fintype.card n - 1)
<VAR>R : Type u<VAR>CommRing R<VAR>n : Type v<VAR>DecidableEq n<VAR>Fintype n<VAR>M : Matrix n n R<VAR>k : ℕ<VAR>h : Fintype.card n - 1 ≤ k<GOAL>M.charpoly.coeff k = (∏ i : n, (Polynomial.X - Polynomial.C (M i i))).coeff k
<VAR>R : Type u<VAR>CommRing R<VAR>n : Type v<VAR>DecidableEq n<VAR>Fintype n<VAR>h : Fintype.card n = 0<VAR>M : Matrix n n R<GOAL>M.det = 1
<VAR>R : Type u<VAR>CommRing R<VAR>n : Type v<VAR>DecidableEq n<VAR>Fintype n<VAR>Nontrivial R<VAR>M : Matrix n n R<GOAL>M.charpoly.degree = ↑(Fintype.card n)
<VAR>R : Type u<VAR>CommRing R<VAR>n : Type v<VAR>DecidableEq n<VAR>Fintype n<VAR>Nontrivial R<VAR>M : Matrix n n R<GOAL>M.charpoly.natDegree = Fintype.card n
<VAR>R : Type u<VAR>CommRing R<VAR>n : Type v<VAR>DecidableEq n<VAR>Fintype n<VAR>M : Matrix n n R<GOAL>M.charpoly.Monic
<VAR>R : Type u<VAR>CommRing R<VAR>n : Type v<VAR>DecidableEq n<VAR>Fintype n<VAR>Nonempty n<VAR>M : Matrix n n R<GOAL>M.trace = -M.charpoly.coeff (Fintype.card n - 1)
<VAR>R : Type u<VAR>CommRing R<VAR>n : Type v<VAR>DecidableEq n<VAR>Fintype n<VAR>M : (Matrix n n R)[X]<VAR>r : R<GOAL>(matPolyEquiv.symm M).map (Polynomial.eval r) = Polynomial.eval ((Matrix.scalar n) r) M
<VAR>R : Type u<VAR>CommRing R<VAR>n : Type v<VAR>DecidableEq n<VAR>Fintype n<VAR>M : Matrix n n R[X]<VAR>r : R<GOAL>Polynomial.eval ((Matrix.scalar n) r) (matPolyEquiv M) = M.map (Polynomial.eval r)
<VAR>R : Type u<VAR>CommRing R<VAR>n : Type v<VAR>DecidableEq n<VAR>Fintype n<VAR>M : Matrix n n R[X]<VAR>r : R<VAR>i j : n<GOAL>Polynomial.eval ((Matrix.scalar n) r) (matPolyEquiv M) i j = Polynomial.eval r (M i j)
<VAR>R : Type u<VAR>CommRing R<VAR>n : Type v<VAR>DecidableEq n<VAR>Fintype n<VAR>M : Matrix n n R[X]<VAR>r : R<GOAL>Polynomial.eval r M.det = (Polynomial.eval ((Matrix.scalar n) r) (matPolyEquiv M)).det
<VAR>R : Type u<VAR>CommRing R<VAR>n : Type v<VAR>DecidableEq n<VAR>Fintype n<VAR>M : Matrix n n R<GOAL>M.det = (-1) ^ Fintype.card n * M.charpoly.coeff 0
<VAR>R : Type u<VAR>CommRing R<VAR>n : Type v<VAR>DecidableEq n<VAR>Fintype n<VAR>A : Matrix n n R[X]<VAR>M : Matrix n n R<GOAL>Polynomial.eval 0 (A + Polynomial.X • M.map ⇑Polynomial.C).det = Polynomial.eval 0 A.det
<VAR>R : Type u<VAR>CommRing R<VAR>n : ℕ<VAR>M : Matrix (Fin n) (Fin n) R<GOAL>Polynomial.eval 0 (Polynomial.derivative (1 + Polynomial.X • M.map ⇑Polynomial.C).det) = M.trace
<VAR>R : Type u<VAR>CommRing R<VAR>n : Type v<VAR>DecidableEq n<VAR>Fintype n<VAR>M : Matrix n n R<GOAL>Polynomial.eval 0 (Polynomial.derivative (1 + Polynomial.X • M.map ⇑Polynomial.C).det) = M.trace
<VAR>R : Type u<VAR>CommRing R<VAR>n : Type v<VAR>DecidableEq n<VAR>Fintype n<VAR>M : Matrix n n R<GOAL>(1 + Polynomial.X • M.map ⇑Polynomial.C).det.coeff 1 = M.trace
<VAR>R : Type u<VAR>CommRing R<VAR>n : Type v<VAR>DecidableEq n<VAR>Fintype n<VAR>M : Matrix n n R<GOAL>(1 + Polynomial.X • M.map ⇑Polynomial.C).det = 1 + M.trace • Polynomial.X + (1 + Polynomial.X • M.map ⇑Polynomial.C).det.divX.divX * Polynomial.X ^ 2
<VAR>R : Type u<VAR>CommRing R<VAR>n : Type v<VAR>DecidableEq n<VAR>Fintype n<VAR>r : R<VAR>M : Matrix n n R<GOAL>(1 + r • M).det = 1 + M.trace * r + Polynomial.eval r (1 + Polynomial.X • M.map ⇑Polynomial.C).det.divX.divX * r ^ 2
<VAR>n : Type v<VAR>DecidableEq n<VAR>Fintype n<VAR>K : Type u_1<VAR>k : ℕ<VAR>Field K<VAR>M : Matrix n n K<GOAL>matPolyEquiv ((↑(Polynomial.expand K k)).mapMatrix (M ^ k).charmatrix) = Polynomial.X ^ k - Polynomial.C (M ^ k)
<VAR>R : Type u<VAR>CommRing R<VAR>n : Type v<VAR>DecidableEq n<VAR>Fintype n<VAR>M : Matrix n n R<VAR>p : R[X]<GOAL>(Polynomial.aeval M) p = (Polynomial.aeval M) (p %ₘ M.charpoly)
<VAR>R : Type u<VAR>CommRing R<VAR>n : Type v<VAR>DecidableEq n<VAR>Fintype n<VAR>M : Matrix n n R<VAR>k : ℕ<GOAL>M ^ k = (Polynomial.aeval M) (Polynomial.X ^ k %ₘ M.charpoly)
<VAR>R : Type u<VAR>CommRing R<VAR>n : Type v<VAR>DecidableEq n<VAR>Fintype n<VAR>M : Matrix n n R<VAR>I : Ideal R<VAR>h : ∀ (i j : n), M i j ∈ I<VAR>k : ℕ<GOAL>M.charpoly.coeff k ∈ I ^ (Fintype.card n - k)
<VAR>R : Type u<VAR>CommRing R<VAR>n : Type v<VAR>DecidableEq n<VAR>Fintype n<VAR>M : Matrix n n R<GOAL>M.charpoly.reverse = M.charpolyRev
<VAR>R : Type u<VAR>CommRing R<VAR>n : Type v<VAR>DecidableEq n<VAR>Fintype n<VAR>M : Matrix n n R<GOAL>Polynomial.eval 0 M.charpolyRev = 1
<VAR>R : Type u<VAR>CommRing R<VAR>n : Type v<VAR>DecidableEq n<VAR>Fintype n<VAR>M : Matrix n n R<GOAL>M.charpolyRev.coeff 1 = -M.trace
<VAR>R : Type u<VAR>CommRing R<VAR>n : Type v<VAR>DecidableEq n<VAR>Fintype n<VAR>M : Matrix n n R<VAR>hM : IsNilpotent M<GOAL>IsUnit M.charpolyRev
<VAR>R : Type u<VAR>CommRing R<VAR>n : Type v<VAR>DecidableEq n<VAR>Fintype n<VAR>M : Matrix n n R<VAR>hM : IsNilpotent M<GOAL>IsNilpotent M.trace
<VAR>R : Type u<VAR>CommRing R<VAR>n : Type v<VAR>DecidableEq n<VAR>Fintype n<VAR>M : Matrix n n R<VAR>hM : IsNilpotent M<GOAL>IsNilpotent (M.charpoly - Polynomial.X ^ Fintype.card n)
<VAR>R : Type v<VAR>inst : Ring R<VAR>self : HasRankNullity.{u, v} R<VAR>M : Type u<VAR>AddCommGroup M<VAR>Module R M<GOAL>∃ s, #↑s = Module.rank R M ∧ LinearIndependent (ι := ↑s) R Subtype.val
<VAR>R : Type v<VAR>inst : Ring R<VAR>self : HasRankNullity.{u, v} R<VAR>M : Type u<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Submodule R M<GOAL>Module.rank R (M ⧸ N) + Module.rank R ↥N = Module.rank R M
<VAR>R : Type u_1<VAR>M : Type u<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>HasRankNullity.{u, u_1} R<VAR>N : Submodule R M<GOAL>Module.rank R (M ⧸ N) + Module.rank R ↥N = Module.rank R M
<VAR>R : Type u_1<VAR>M : Type u<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>HasRankNullity.{u, u_1} R<GOAL>∃ s, #↑s = Module.rank R M ∧ LinearIndependent (ι := ↑s) R Subtype.val
<VAR>R : Type u_1<VAR>Ring R<VAR>HasRankNullity.{u, u_1} R<GOAL>Nontrivial R
<VAR>R : Type u_1<VAR>M : Type u<VAR>M' : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>AddCommGroup M'<VAR>Module R M<VAR>Module R M'<VAR>HasRankNullity.{u, u_1} R<VAR>f : M →ₗ[R] M'<GOAL>Cardinal.lift.{u, v} (Module.rank R ↥(LinearMap.range f)) + Cardinal.lift.{v, u} (Module.rank R ↥(LinearMap.ker f)) = Cardinal.lift.{v, u} (Module.rank R M)
<VAR>R : Type u_1<VAR>M M₁ : Type u<VAR>Ring R<VAR>AddCommGroup M<VAR>AddCommGroup M₁<VAR>Module R M<VAR>Module R M₁<VAR>HasRankNullity.{u, u_1} R<VAR>f : M →ₗ[R] M₁<GOAL>Module.rank R ↥(LinearMap.range f) + Module.rank R ↥(LinearMap.ker f) = Module.rank R M
<VAR>R : Type u_1<VAR>M : Type u<VAR>M' : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>AddCommGroup M'<VAR>Module R M<VAR>Module R M'<VAR>HasRankNullity.{u, u_1} R<VAR>f : M →ₗ[R] M'<VAR>h : Function.Surjective ⇑f<GOAL>Cardinal.lift.{v, u} (Module.rank R M) = Cardinal.lift.{u, v} (Module.rank R M') + Cardinal.lift.{v, u} (Module.rank R ↥(LinearMap.ker f))
<VAR>R : Type u_1<VAR>M M₁ : Type u<VAR>Ring R<VAR>AddCommGroup M<VAR>AddCommGroup M₁<VAR>Module R M<VAR>Module R M₁<VAR>HasRankNullity.{u, u_1} R<VAR>f : M →ₗ[R] M₁<VAR>h : Function.Surjective ⇑f<GOAL>Module.rank R M = Module.rank R M₁ + Module.rank R ↥(LinearMap.ker f)
<VAR>R : Type u_1<VAR>M : Type u<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>HasRankNullity.{u, u_1} R<VAR>StrongRankCondition R<VAR>s : Set M<VAR>hs : LinearIndependent (ι := ↑s) R Subtype.val<GOAL>∃ t, s ⊆ t ∧ #↑t = Module.rank R M ∧ LinearIndependent (ι := ↑t) R Subtype.val
<VAR>R : Type u_1<VAR>M : Type u<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>HasRankNullity.{u, u_1} R<VAR>StrongRankCondition R<VAR>n : ℕ<VAR>v : Fin n → M<VAR>hv : LinearIndependent R v<VAR>h : ↑n < Module.rank R M<GOAL>∃ x, LinearIndependent R (Fin.cons x v)
<VAR>R : Type u_1<VAR>M : Type u<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>HasRankNullity.{u, u_1} R<VAR>StrongRankCondition R<VAR>n : ℕ<VAR>v : Fin n → M<VAR>hv : LinearIndependent R v<VAR>h : ↑n < Module.rank R M<GOAL>∃ x, LinearIndependent R (Fin.snoc v x)
<VAR>R : Type u_1<VAR>M : Type u<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>HasRankNullity.{u, u_1} R<VAR>StrongRankCondition R<VAR>NoZeroSMulDivisors R M<VAR>h : 1 < Module.rank R M<VAR>x : M<VAR>hx : x ≠ 0<GOAL>∃ y, LinearIndependent R ![x, y]
<VAR>R : Type u_1<VAR>M : Type u<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>HasRankNullity.{u, u_1} R<VAR>N : Submodule R M<VAR>h : Module.rank R ↥N < Module.rank R M<GOAL>∃ m, ∀ (r : R), r ≠ 0 → r • m ∉ N
<VAR>R : Type u_1<VAR>M : Type u<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>HasRankNullity.{u, u_1} R<VAR>s t : Submodule R M<GOAL>Module.rank R ↥(s ⊔ t) + Module.rank R ↥(s ⊓ t) = Module.rank R ↥s + Module.rank R ↥t
<VAR>R : Type u_1<VAR>M : Type u<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>HasRankNullity.{u, u_1} R<VAR>s t : Submodule R M<GOAL>Module.rank R ↥(s ⊔ t) ≤ Module.rank R ↥s + Module.rank R ↥t
<VAR>R : Type u_1<VAR>M : Type u<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>HasRankNullity.{u, u_1} R<VAR>StrongRankCondition R<VAR>n : ℕ<VAR>v : Fin n → M<VAR>hv : LinearIndependent R v<VAR>h : n < FiniteDimensional.finrank R M<GOAL>∃ x, LinearIndependent R (Fin.snoc v x)
<VAR>R : Type u_1<VAR>M : Type u<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>HasRankNullity.{u, u_1} R<VAR>StrongRankCondition R<VAR>n : ℕ<VAR>v : Fin n → M<VAR>hv : LinearIndependent R v<VAR>h : n < FiniteDimensional.finrank R M<GOAL>∃ x, LinearIndependent R (Fin.cons x v)
<VAR>R : Type u_1<VAR>M : Type u<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>HasRankNullity.{u, u_1} R<VAR>StrongRankCondition R<VAR>NoZeroSMulDivisors R M<VAR>h : 1 < FiniteDimensional.finrank R M<VAR>x : M<VAR>hx : x ≠ 0<GOAL>∃ y, LinearIndependent R ![x, y]
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N<VAR>m : M<GOAL>(ExteriorAlgebra.liftAlternating f) ((ExteriorAlgebra.ι R) m) = (f 1) ![m]
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N<VAR>m : M<VAR>x : ExteriorAlgebra R M<GOAL>(ExteriorAlgebra.liftAlternating f) ((ExteriorAlgebra.ι R) m * x) = (ExteriorAlgebra.liftAlternating fun i => (f i.succ).curryLeft m) x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N<GOAL>(ExteriorAlgebra.liftAlternating f) 1 = (f 0) 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N<VAR>r : R<GOAL>(ExteriorAlgebra.liftAlternating f) ((algebraMap R (ExteriorAlgebra R M)) r) = r • (f 0) 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>n : ℕ<VAR>f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N<VAR>v : Fin n → M<GOAL>(ExteriorAlgebra.liftAlternating f) ((ExteriorAlgebra.ιMulti R n) v) = (f n) v
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>n : ℕ<VAR>f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N<GOAL>(ExteriorAlgebra.liftAlternating f).compAlternatingMap (ExteriorAlgebra.ιMulti R n) = f n
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>N' : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>AddCommGroup N'<VAR>Module R M<VAR>Module R N<VAR>Module R N'<VAR>g : N →ₗ[R] N'<VAR>f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N<GOAL>(ExteriorAlgebra.liftAlternating fun i => g.compAlternatingMap (f i)) = g ∘ₗ ExteriorAlgebra.liftAlternating f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<GOAL>ExteriorAlgebra.liftAlternating (ExteriorAlgebra.ιMulti R) = LinearMap.id
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>F : ExteriorAlgebra R M →ₗ[R] N<VAR>i : ℕ<GOAL>ExteriorAlgebra.liftAlternatingEquiv.symm F i = F.compAlternatingMap (ExteriorAlgebra.ιMulti R i)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N<GOAL>ExteriorAlgebra.liftAlternatingEquiv a = ExteriorAlgebra.liftAlternating a
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>f g : ExteriorAlgebra R M →ₗ[R] N<VAR>h : ∀ (i : ℕ), f.compAlternatingMap (ExteriorAlgebra.ιMulti R i) = g.compAlternatingMap (ExteriorAlgebra.ιMulti R i)<GOAL>f = g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>N : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>g : N →ₗ[R] P<VAR>q : Q<GOAL>LinearMap.range g ≤ Submodule.comap ((TensorProduct.mk R Q P) q) (LinearMap.range (LinearMap.lTensor Q g))
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>N : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>g : N →ₗ[R] P<VAR>q : Q<GOAL>LinearMap.range g ≤ Submodule.comap ((TensorProduct.mk R P Q).flip q) (LinearMap.range (LinearMap.rTensor Q g))
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>N : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>g : N →ₗ[R] P<VAR>hg : Function.Surjective ⇑g<GOAL>Function.Surjective ⇑(LinearMap.lTensor Q g)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>N : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>g : N →ₗ[R] P<GOAL>LinearMap.range (LinearMap.lTensor Q g) = LinearMap.range (LinearMap.lTensor Q (LinearMap.range g).subtype)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>N : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>g : N →ₗ[R] P<VAR>hg : Function.Surjective ⇑g<GOAL>Function.Surjective ⇑(LinearMap.rTensor Q g)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>N : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>g : N →ₗ[R] P<GOAL>LinearMap.range (LinearMap.rTensor Q g) = LinearMap.range (LinearMap.rTensor Q (LinearMap.range g).subtype)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>AddCommGroup P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>AddCommGroup Q<VAR>Module R Q<VAR>hfg : Function.Exact ⇑f ⇑g<VAR>h : P → N<VAR>hgh : Function.RightInverse h ⇑g<VAR>y : TensorProduct R Q N<GOAL>(lTensor.inverse_of_rightInverse Q hfg hgh) ((LinearMap.lTensor Q g) y) = Submodule.Quotient.mk y
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>AddCommGroup P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>AddCommGroup Q<VAR>Module R Q<VAR>hfg : Function.Exact ⇑f ⇑g<VAR>h : P → N<VAR>hgh : Function.RightInverse h ⇑g<GOAL>lTensor.inverse_of_rightInverse Q hfg hgh ∘ₗ LinearMap.lTensor Q g = (LinearMap.range (LinearMap.lTensor Q f)).mkQ
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>AddCommGroup P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>AddCommGroup Q<VAR>Module R Q<VAR>hfg : Function.Exact ⇑f ⇑g<VAR>hg : Function.Surjective ⇑g<VAR>y : TensorProduct R Q N<GOAL>(lTensor.inverse Q hfg hg) ((LinearMap.lTensor Q g) y) = Submodule.Quotient.mk y
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>AddCommGroup P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>AddCommGroup Q<VAR>Module R Q<VAR>hfg : Function.Exact ⇑f ⇑g<VAR>hg : Function.Surjective ⇑g<GOAL>lTensor.inverse Q hfg hg ∘ₗ LinearMap.lTensor Q g = (LinearMap.range (LinearMap.lTensor Q f)).mkQ
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>AddCommGroup P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>AddCommGroup Q<VAR>Module R Q<VAR>hfg : Function.Exact ⇑f ⇑g<VAR>hg : Function.Surjective ⇑g<GOAL>Function.Exact ⇑(LinearMap.lTensor Q f) ⇑(LinearMap.lTensor Q g)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : Type u_5<VAR>AddCommGroup Q<VAR>Module R Q<VAR>N : Submodule R M<GOAL>LinearMap.ker (LinearMap.lTensor Q N.mkQ) = LinearMap.range (LinearMap.lTensor Q N.subtype)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>AddCommGroup P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>AddCommGroup Q<VAR>Module R Q<VAR>hfg : Function.Exact ⇑f ⇑g<VAR>h : P → N<VAR>hgh : Function.RightInverse h ⇑g<VAR>y : TensorProduct R N Q<GOAL>(rTensor.inverse_of_rightInverse Q hfg hgh) ((LinearMap.rTensor Q g) y) = Submodule.Quotient.mk y
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>AddCommGroup P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>AddCommGroup Q<VAR>Module R Q<VAR>hfg : Function.Exact ⇑f ⇑g<VAR>h : P → N<VAR>hgh : Function.RightInverse h ⇑g<GOAL>rTensor.inverse_of_rightInverse Q hfg hgh ∘ₗ LinearMap.rTensor Q g = (LinearMap.range (LinearMap.rTensor Q f)).mkQ
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>AddCommGroup P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>AddCommGroup Q<VAR>Module R Q<VAR>hfg : Function.Exact ⇑f ⇑g<VAR>hg : Function.Surjective ⇑g<VAR>y : TensorProduct R N Q<GOAL>(rTensor.inverse Q hfg hg) ((LinearMap.rTensor Q g) y) = Submodule.Quotient.mk y