ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>AddCommGroup N<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R N<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>Qₙ : QuadraticForm R N<VAR>f₁ : Q₁ →qᵢ Qₙ<VAR>f₂ : Q₂ →qᵢ Qₙ<VAR>hf : ∀ (x : M₁) (y : M₂), QuadraticMap.IsOrtho Qₙ (f₁ x) (f₂ y)<VAR>m₁ : CliffordAlgebra Q₁<VAR>m₂ : CliffordAlgebra Q₂<VAR>i₁ i₂ : ZMod 2<VAR>hm₁ : m₁ ∈ CliffordAlgebra.evenOdd Q₁ i₁<VAR>hm₂ : m₂ ∈ CliffordAlgebra.evenOdd Q₂ i₂<GOAL>(CliffordAlgebra.map f₁) m₁ * (CliffordAlgebra.map f₂) m₂ = (-1) ^ (i₂ * i₁) • ((CliffordAlgebra.map f₂) m₂ * (CliffordAlgebra.map f₁) m₁)
<VAR>R : Type u_1<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>AddCommGroup N<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R N<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>Qₙ : QuadraticForm R N<VAR>f₁ : Q₁ →qᵢ Qₙ<VAR>f₂ : Q₂ →qᵢ Qₙ<VAR>hf : ∀ (x : M₁) (y : M₂), QuadraticMap.IsOrtho Qₙ (f₁ x) (f₂ y)<VAR>m₁ : CliffordAlgebra Q₁<VAR>m₂ : CliffordAlgebra Q₂<VAR>i₂ : ZMod 2<VAR>hm₁ : m₁ ∈ CliffordAlgebra.evenOdd Q₁ 0<VAR>hm₂ : m₂ ∈ CliffordAlgebra.evenOdd Q₂ i₂<GOAL>Commute ((CliffordAlgebra.map f₁) m₁) ((CliffordAlgebra.map f₂) m₂)
<VAR>R : Type u_1<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>AddCommGroup N<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R N<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>Qₙ : QuadraticForm R N<VAR>f₁ : Q₁ →qᵢ Qₙ<VAR>f₂ : Q₂ →qᵢ Qₙ<VAR>hf : ∀ (x : M₁) (y : M₂), QuadraticMap.IsOrtho Qₙ (f₁ x) (f₂ y)<VAR>m₁ : CliffordAlgebra Q₁<VAR>m₂ : CliffordAlgebra Q₂<VAR>i₁ : ZMod 2<VAR>hm₁ : m₁ ∈ CliffordAlgebra.evenOdd Q₁ i₁<VAR>hm₂ : m₂ ∈ CliffordAlgebra.evenOdd Q₂ 0<GOAL>Commute ((CliffordAlgebra.map f₁) m₁) ((CliffordAlgebra.map f₂) m₂)
<VAR>R : Type u_1<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>N : Type u_4<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>AddCommGroup N<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R N<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>Qₙ : QuadraticForm R N<VAR>f₁ : Q₁ →qᵢ Qₙ<VAR>f₂ : Q₂ →qᵢ Qₙ<VAR>hf : ∀ (x : M₁) (y : M₂), QuadraticMap.IsOrtho Qₙ (f₁ x) (f₂ y)<VAR>m₁ : CliffordAlgebra Q₁<VAR>m₂ : CliffordAlgebra Q₂<VAR>hm₁ : m₁ ∈ CliffordAlgebra.evenOdd Q₁ 1<VAR>hm₂ : m₂ ∈ CliffordAlgebra.evenOdd Q₂ 1<GOAL>(CliffordAlgebra.map f₁) m₁ * (CliffordAlgebra.map f₂) m₂ = -(CliffordAlgebra.map f₂) m₂ * (CliffordAlgebra.map f₁) m₁
<VAR>R : Type u_1<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>m₁ : M₁<VAR>m₂ : M₂<GOAL>(CliffordAlgebra.ofProd Q₁ Q₂) ((CliffordAlgebra.ι (QuadraticMap.prod Q₁ Q₂)) (m₁, m₂)) = (CliffordAlgebra.ι Q₁) m₁ ᵍ⊗ₜ[R] 1 + 1 ᵍ⊗ₜ[R] (CliffordAlgebra.ι Q₂) m₂
<VAR>R : Type u_1<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>m₁ : M₁<GOAL>(CliffordAlgebra.toProd Q₁ Q₂) ((CliffordAlgebra.ι Q₁) m₁ ᵍ⊗ₜ[R] 1) = (CliffordAlgebra.ι (QuadraticMap.prod Q₁ Q₂)) (m₁, 0)
<VAR>R : Type u_1<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>m₂ : M₂<GOAL>(CliffordAlgebra.toProd Q₁ Q₂) (1 ᵍ⊗ₜ[R] (CliffordAlgebra.ι Q₂) m₂) = (CliffordAlgebra.ι (QuadraticMap.prod Q₁ Q₂)) (0, m₂)
<VAR>R : Type u_1<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<GOAL>(CliffordAlgebra.toProd Q₁ Q₂).comp (CliffordAlgebra.ofProd Q₁ Q₂) = AlgHom.id R (CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))
<VAR>R : Type u_1<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<GOAL>(CliffordAlgebra.ofProd Q₁ Q₂).comp (CliffordAlgebra.toProd Q₁ Q₂) = AlgHom.id R (CliffordAlgebra.evenOdd Q₁ ᵍ⊗[R] CliffordAlgebra.evenOdd Q₂)
<VAR>R : Type u_1<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>a : CliffordAlgebra.evenOdd Q₁ ᵍ⊗[R] CliffordAlgebra.evenOdd Q₂<GOAL>(CliffordAlgebra.prodEquiv Q₁ Q₂).symm a = (CliffordAlgebra.toProd Q₁ Q₂) a
<VAR>R : Type u_1<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>a : CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)<GOAL>(CliffordAlgebra.prodEquiv Q₁ Q₂) a = (CliffordAlgebra.ofProd Q₁ Q₂) a
<VAR>R : Type u<VAR>CommRing R<VAR>Invertible 2<GOAL>(QuadraticModuleCat.toModuleCatBraidedFunctor R).toMonoidalFunctor = QuadraticModuleCat.toModuleCatMonoidalFunctor R
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<VAR>x y : M<GOAL>Setoid.r x y ↔ x - y ∈ p
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<VAR>x : M<GOAL>Quotient.mk' x = Submodule.Quotient.mk x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<VAR>x : M<GOAL>Quotient.mk'' x = Submodule.Quotient.mk x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<VAR>x : M<GOAL>Quot.mk Setoid.r x = Submodule.Quotient.mk x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<VAR>x y : M<GOAL>Submodule.Quotient.mk x = Submodule.Quotient.mk y ↔ -x + y ∈ p
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<VAR>x y : M<GOAL>Submodule.Quotient.mk x = Submodule.Quotient.mk y ↔ x - y ∈ p
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<GOAL>Submodule.Quotient.mk 0 = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>x : M<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<GOAL>Submodule.Quotient.mk x = 0 ↔ x ∈ p
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>x y : M<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<GOAL>Submodule.Quotient.mk (x + y) = Submodule.Quotient.mk x + Submodule.Quotient.mk y
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>x : M<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<GOAL>Submodule.Quotient.mk (-x) = -Submodule.Quotient.mk x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>x y : M<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<GOAL>Submodule.Quotient.mk (x - y) = Submodule.Quotient.mk x - Submodule.Quotient.mk y
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<VAR>S : Type u_3<VAR>SMul S R<VAR>SMul S M<VAR>IsScalarTower S R M<VAR>r : S<VAR>x : M<GOAL>Submodule.Quotient.mk (r • x) = r • Submodule.Quotient.mk x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>S : Type u_3<VAR>Ring S<VAR>SMul S R<VAR>Module S M<VAR>IsScalarTower S R M<VAR>P : Submodule R M<VAR>x : M<GOAL>(Submodule.Quotient.restrictScalarsEquiv S P) (Submodule.Quotient.mk x) = Submodule.Quotient.mk x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>S : Type u_3<VAR>Ring S<VAR>SMul S R<VAR>Module S M<VAR>IsScalarTower S R M<VAR>P : Submodule R M<VAR>x : M<GOAL>(Submodule.Quotient.restrictScalarsEquiv S P).symm (Submodule.Quotient.mk x) = Submodule.Quotient.mk x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<GOAL>Function.Surjective Submodule.Quotient.mk
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<VAR>h : p < ⊤<GOAL>Nontrivial (M ⧸ p)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<GOAL>Subsingleton (M ⧸ p) ↔ p = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<GOAL>Nonempty (Unique (M ⧸ p)) ↔ p = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>S : Submodule R M<GOAL>Nat.card M = Nat.card ↥S * Nat.card (M ⧸ S)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<VAR>M₂ : Type u_3<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>f g : M ⧸ p →ₗ[R] M₂<VAR>h : ∀ (x : M), f (Submodule.Quotient.mk x) = g (Submodule.Quotient.mk x)<GOAL>f = g
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<VAR>x : M<GOAL>p.mkQ x = Submodule.Quotient.mk x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>A : Submodule R M<GOAL>Function.Surjective ⇑A.mkQ
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<VAR>R₂ : Type u_3<VAR>M₂ : Type u_4<VAR>Ring R₂<VAR>AddCommGroup M₂<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>f g : M ⧸ p →ₛₗ[τ₁₂] M₂<VAR>h : f.comp p.mkQ = g.comp p.mkQ<GOAL>f = g
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<VAR>R₂ : Type u_3<VAR>M₂ : Type u_4<VAR>Ring R₂<VAR>AddCommGroup M₂<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>h : p ≤ LinearMap.ker f<VAR>x : M<GOAL>(p.liftQ f h) (Submodule.Quotient.mk x) = f x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<VAR>R₂ : Type u_3<VAR>M₂ : Type u_4<VAR>Ring R₂<VAR>AddCommGroup M₂<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>h : p ≤ LinearMap.ker f<GOAL>(p.liftQ f h).comp p.mkQ = f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>R₂ : Type u_3<VAR>M₂ : Type u_4<VAR>Ring R₂<VAR>AddCommGroup M₂<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>x : M<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>h : f x = 0<VAR>y : M<GOAL>(Submodule.liftQSpanSingleton x f h) (Submodule.Quotient.mk y) = f y
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<GOAL>LinearMap.range p.mkQ = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<GOAL>LinearMap.ker p.mkQ = p
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<VAR>p' : Submodule R (M ⧸ p)<GOAL>p ≤ Submodule.comap p.mkQ p'
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<GOAL>Submodule.map p.mkQ p = ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p p' : Submodule R M<GOAL>Submodule.comap p.mkQ (Submodule.map p.mkQ p') = p ⊔ p'
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p p' : Submodule R M<GOAL>Submodule.map p.mkQ p' = ⊤ ↔ p ⊔ p' = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<VAR>R₂ : Type u_3<VAR>M₂ : Type u_4<VAR>Ring R₂<VAR>AddCommGroup M₂<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>q : Submodule R₂ M₂<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>h : p ≤ Submodule.comap f q<VAR>x : M<GOAL>(p.mapQ q f h) (Submodule.Quotient.mk x) = Submodule.Quotient.mk (f x)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<VAR>R₂ : Type u_3<VAR>M₂ : Type u_4<VAR>Ring R₂<VAR>AddCommGroup M₂<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>q : Submodule R₂ M₂<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>h : p ≤ Submodule.comap f q<GOAL>(p.mapQ q f h).comp p.mkQ = q.mkQ.comp f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<VAR>R₂ : Type u_3<VAR>M₂ : Type u_4<VAR>Ring R₂<VAR>AddCommGroup M₂<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>q : Submodule R₂ M₂<VAR>h : p ≤ Submodule.comap 0 q := ⋯<GOAL>p.mapQ q 0 h = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<VAR>R₂ : Type u_3<VAR>M₂ : Type u_4<VAR>Ring R₂<VAR>AddCommGroup M₂<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>R₃ : Type u_5<VAR>M₃ : Type u_6<VAR>Ring R₃<VAR>AddCommGroup M₃<VAR>Module R₃ M₃<VAR>p₂ : Submodule R₂ M₂<VAR>p₃ : Submodule R₃ M₃<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>g : M₂ →ₛₗ[τ₂₃] M₃<VAR>hf : p ≤ Submodule.comap f p₂<VAR>hg : p₂ ≤ Submodule.comap g p₃<VAR>h : p ≤ Submodule.comap f (Submodule.comap g p₃) := ⋯<GOAL>p.mapQ p₃ (g.comp f) h = (p₂.mapQ p₃ g hg).comp (p.mapQ p₂ f hf)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<VAR>h : p ≤ Submodule.comap LinearMap.id p := ⋯<GOAL>p.mapQ p LinearMap.id h = LinearMap.id
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<VAR>f : M →ₗ[R] M<VAR>h : p ≤ Submodule.comap f p<VAR>k : ℕ<VAR>h' : p ≤ Submodule.comap (f ^ k) p := ⋯<GOAL>p.mapQ p (f ^ k) h' = p.mapQ p f h ^ k
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<VAR>R₂ : Type u_3<VAR>M₂ : Type u_4<VAR>Ring R₂<VAR>AddCommGroup M₂<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>q : Submodule R₂ M₂<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>h : p ≤ LinearMap.ker f<GOAL>Submodule.comap (p.liftQ f h) q = Submodule.map p.mkQ (Submodule.comap f q)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<VAR>R₂ : Type u_3<VAR>M₂ : Type u_4<VAR>Ring R₂<VAR>AddCommGroup M₂<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>RingHomSurjective τ₁₂<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>h : p ≤ LinearMap.ker f<VAR>q : Submodule R (M ⧸ p)<GOAL>Submodule.map (p.liftQ f h) q = Submodule.map f (Submodule.comap p.mkQ q)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<VAR>R₂ : Type u_3<VAR>M₂ : Type u_4<VAR>Ring R₂<VAR>AddCommGroup M₂<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>h : p ≤ LinearMap.ker f<GOAL>LinearMap.ker (p.liftQ f h) = Submodule.map p.mkQ (LinearMap.ker f)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<VAR>R₂ : Type u_3<VAR>M₂ : Type u_4<VAR>Ring R₂<VAR>AddCommGroup M₂<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>RingHomSurjective τ₁₂<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>h : p ≤ LinearMap.ker f<GOAL>LinearMap.range (p.liftQ f h) = LinearMap.range f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<VAR>R₂ : Type u_3<VAR>M₂ : Type u_4<VAR>Ring R₂<VAR>AddCommGroup M₂<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>h : p ≤ LinearMap.ker f<VAR>h' : LinearMap.ker f ≤ p<GOAL>LinearMap.ker (p.liftQ f h) = ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<VAR>R₂ : Type u_3<VAR>M₂ : Type u_4<VAR>Ring R₂<VAR>AddCommGroup M₂<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>h : p = LinearMap.ker f<GOAL>LinearMap.ker (p.liftQ f ⋯) = ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<VAR>p' : Submodule R (M ⧸ p)<GOAL>p.comapMkQOrderEmbedding p' = Submodule.comap p.mkQ p'
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>R₂ : Type u_3<VAR>M₂ : Type u_4<VAR>Ring R₂<VAR>AddCommGroup M₂<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>RingHomSurjective τ₁₂<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>s : Set M₂<VAR>h₀ : s.Nonempty<VAR>h₁ : s ⊆ ↑(LinearMap.range f)<GOAL>Submodule.span R (⇑f ⁻¹' s) = Submodule.comap f (Submodule.span R₂ s)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_5<VAR>AddCommGroup N<VAR>Module R N<VAR>P : Submodule R M<VAR>Q : Submodule R N<VAR>f : M ≃ₗ[R] N<VAR>hf : Submodule.map f P = Q<VAR>a : N ⧸ Q<GOAL>(Submodule.Quotient.equiv P Q f hf).symm a = (Q.mapQ P ↑f.symm ⋯) a
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_5<VAR>AddCommGroup N<VAR>Module R N<VAR>P : Submodule R M<VAR>Q : Submodule R N<VAR>f : M ≃ₗ[R] N<VAR>hf : Submodule.map f P = Q<VAR>a : M ⧸ P<GOAL>(Submodule.Quotient.equiv P Q f hf) a = (P.mapQ Q ↑f ⋯) a
<VAR>R : Type u_5<VAR>M : Type u_6<VAR>N : Type u_7<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>P : Submodule R M<VAR>Q : Submodule R N<VAR>f : M ≃ₗ[R] N<VAR>hf : Submodule.map f P = Q<GOAL>(Submodule.Quotient.equiv P Q f hf).symm = Submodule.Quotient.equiv Q P f.symm ⋯
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_5<VAR>O : Type u_6<VAR>AddCommGroup N<VAR>Module R N<VAR>AddCommGroup O<VAR>Module R O<VAR>P : Submodule R M<VAR>Q : Submodule R N<VAR>S : Submodule R O<VAR>e : M ≃ₗ[R] N<VAR>f : N ≃ₗ[R] O<VAR>he : Submodule.map e P = Q<VAR>hf : Submodule.map f Q = S<VAR>hef : Submodule.map (e ≪≫ₗ f) P = S<GOAL>Submodule.Quotient.equiv P S (e ≪≫ₗ f) hef = Submodule.Quotient.equiv P Q e he ≪≫ₗ Submodule.Quotient.equiv Q S f hf
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>R₂ : Type u_3<VAR>M₂ : Type u_4<VAR>Ring R<VAR>Ring R₂<VAR>AddCommMonoid M<VAR>AddCommGroup M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>RingHomSurjective τ₁₂<VAR>f : M →ₛₗ[τ₁₂] M₂<GOAL>(LinearMap.range f).mkQ.comp f = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>R₂ : Type u_3<VAR>M₂ : Type u_4<VAR>R₃ : Type u_5<VAR>M₃ : Type u_6<VAR>Ring R<VAR>Ring R₂<VAR>Ring R₃<VAR>AddCommMonoid M<VAR>AddCommGroup M₂<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module R₂ M₂<VAR>Module R₃ M₃<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>RingHomSurjective τ₁₂<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>g : M₂ →ₛₗ[τ₂₃] M₃<GOAL>LinearMap.ker g ≤ LinearMap.range f ↔ (LinearMap.range f).mkQ ∘ₗ (LinearMap.ker g).subtype = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>R₂ : Type u_3<VAR>M₂ : Type u_4<VAR>Ring R<VAR>Ring R₂<VAR>AddCommMonoid M<VAR>AddCommGroup M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>RingHomSurjective τ₁₂<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>h : ∀ (u v : M₂ →ₗ[R₂] M₂ ⧸ LinearMap.range f), u.comp f = v.comp f → u = v<GOAL>LinearMap.range f = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<VAR>hp : p = ⊥<VAR>x : M<GOAL>(p.quotEquivOfEqBot hp) (Submodule.Quotient.mk x) = x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<VAR>hp : p = ⊥<VAR>x : M<GOAL>(p.quotEquivOfEqBot hp).symm x = Submodule.Quotient.mk x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<VAR>hp : p = ⊥<GOAL>↑(p.quotEquivOfEqBot hp).symm = p.mkQ
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p p' : Submodule R M<VAR>h : p = p'<VAR>x : M<GOAL>(p.quotEquivOfEq p' h) (Submodule.Quotient.mk x) = Submodule.Quotient.mk x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>P Q : Submodule R M<VAR>hf : Submodule.map (↑(LinearEquiv.refl R M)) P = Q<GOAL>Submodule.Quotient.equiv P Q (LinearEquiv.refl R M) hf = P.quotEquivOfEq Q ⋯
<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<GOAL>f.IsSemisimple ↔ ∀ p ≤ Submodule.comap f p, ∃ q ≤ Submodule.comap f q, IsCompl p q
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>IsSemisimpleModule R M<GOAL>Module.End.IsSemisimple 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>IsSemisimpleModule R M<GOAL>Module.End.IsSemisimple LinearMap.id
<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<GOAL>(-f).IsSemisimple ↔ f.IsSemisimple
<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>hn : IsNilpotent f<VAR>hs : f.IsSemisimple<GOAL>f = 0
<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>μ : R<GOAL>(f - (algebraMap R (Module.End R M)) μ).IsSemisimple ↔ f.IsSemisimple
<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>p : Submodule R M<VAR>hp : Set.MapsTo ⇑f ↑p ↑p<VAR>hf : f.IsSemisimple<GOAL>Module.End.IsSemisimple (LinearMap.restrict f hp)
<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>K : Type u_3<VAR>Field K<VAR>Module K M<VAR>f : Module.End K M<VAR>t : K<VAR>ht : t ≠ 0<GOAL>(t • f).IsSemisimple ↔ f.IsSemisimple
<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>K : Type u_3<VAR>Field K<VAR>Module K M<VAR>f : Module.End K M<VAR>t : K<VAR>h : f.IsSemisimple<GOAL>(t • f).IsSemisimple
<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>K : Type u_3<VAR>Field K<VAR>Module K M<VAR>f : Module.End K M<VAR>p : K[X]<VAR>hp : Squarefree p<VAR>hpf : (Polynomial.aeval f) p = 0<GOAL>f.IsSemisimple
<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>K : Type u_3<VAR>Field K<VAR>Module K M<VAR>f : Module.End K M<VAR>FiniteDimensional K M<VAR>hf : f.IsSemisimple<GOAL>Squarefree (minpoly K f)
<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>K : Type u_3<VAR>Field K<VAR>Module K M<VAR>f : Module.End K M<VAR>FiniteDimensional K M<VAR>hf : f.IsSemisimple<VAR>p : K[X]<GOAL>((Polynomial.aeval f) p).IsSemisimple
<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>K : Type u_3<VAR>Field K<VAR>Module K M<VAR>f : Module.End K M<VAR>FiniteDimensional K M<VAR>hf : f.IsSemisimple<VAR>a : Module.End K M<VAR>ha : a ∈ Algebra.adjoin K {f}<GOAL>a.IsSemisimple
<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>K : Type u_3<VAR>Field K<VAR>Module K M<VAR>f : Module.End K M<VAR>FiniteDimensional K M<VAR>hf : f.IsSemisimple<VAR>n : ℕ<GOAL>(f ^ n).IsSemisimple
<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>K : Type u_3<VAR>Field K<VAR>Module K M<VAR>f g : Module.End K M<VAR>FiniteDimensional K M<VAR>PerfectField K<VAR>comm : Commute f g<VAR>hf : f.IsSemisimple<VAR>hg : g.IsSemisimple<VAR>a : Module.End K M<VAR>ha : a ∈ Algebra.adjoin K {f, g}<GOAL>a.IsSemisimple
<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>K : Type u_3<VAR>Field K<VAR>Module K M<VAR>f g : Module.End K M<VAR>FiniteDimensional K M<VAR>PerfectField K<VAR>comm : Commute f g<VAR>hf : f.IsSemisimple<VAR>hg : g.IsSemisimple<GOAL>(f + g).IsSemisimple
<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>K : Type u_3<VAR>Field K<VAR>Module K M<VAR>f g : Module.End K M<VAR>FiniteDimensional K M<VAR>PerfectField K<VAR>comm : Commute f g<VAR>hf : f.IsSemisimple<VAR>hg : g.IsSemisimple<GOAL>(f - g).IsSemisimple
<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>K : Type u_3<VAR>Field K<VAR>Module K M<VAR>f g : Module.End K M<VAR>FiniteDimensional K M<VAR>PerfectField K<VAR>comm : Commute f g<VAR>hf : f.IsSemisimple<VAR>hg : g.IsSemisimple<GOAL>(f * g).IsSemisimple
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>x x' y y' : M<GOAL>x = x' → y = y' → (B x) y = (B x') y'
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>x y z : M<GOAL>(B (x + y)) z = (B x) z + (B y) z
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>a : R<VAR>x y : M<GOAL>(B (a • x)) y = a * (B x) y
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>x y z : M<GOAL>(B x) (y + z) = (B x) y + (B x) z
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>a : R<VAR>x y : M<GOAL>(B x) (a • y) = a * (B x) y
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>x : M<GOAL>(B 0) x = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>x : M<GOAL>(B x) 0 = 0
<VAR>R₁ : Type u_4<VAR>M₁ : Type u_5<VAR>CommRing R₁<VAR>AddCommGroup M₁<VAR>Module R₁ M₁<VAR>B₁ : LinearMap.BilinForm R₁ M₁<VAR>x y : M₁<GOAL>(B₁ (-x)) y = -(B₁ x) y