ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>S : Type u_6<VAR>M : Type u_9<VAR>M₃ : Type u_12<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module S M₃<VAR>σ : R →+* S<GOAL>Function.Injective DFunLike.coe
<VAR>R : Type u_1<VAR>S : Type u_6<VAR>M : Type u_9<VAR>M₃ : Type u_12<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module S M₃<VAR>σ : R →+* S<VAR>f : M →ₛₗ[σ] M₃<VAR>x x' : M<GOAL>x = x' → f x = f x'
<VAR>R : Type u_1<VAR>S : Type u_6<VAR>M : Type u_9<VAR>M₃ : Type u_12<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module S M₃<VAR>σ : R →+* S<VAR>f g : M →ₛₗ[σ] M₃<VAR>h : f = g<VAR>x : M<GOAL>f x = g x
<VAR>R : Type u_1<VAR>S : Type u_6<VAR>M : Type u_9<VAR>M₃ : Type u_12<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module S M₃<VAR>σ : R →+* S<VAR>f g : M →ₛₗ[σ] M₃<GOAL>f = g ↔ ∀ (x : M), f x = g x
<VAR>R : Type u_1<VAR>S : Type u_6<VAR>M : Type u_9<VAR>M₃ : Type u_12<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module S M₃<VAR>σ : R →+* S<VAR>f : M →ₛₗ[σ] M₃<VAR>h : ∀ (m : R) (x : M), (↑f).toFun (m • x) = σ m • (↑f).toFun x<GOAL>{ toAddHom := ↑f, map_smul' := h } = f
<VAR>R : Type u_1<VAR>S : Type u_6<VAR>M : Type u_9<VAR>M₃ : Type u_12<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module S M₃<VAR>σ : R →+* S<VAR>f : M →ₛₗ[σ] M₃<VAR>x y : M<GOAL>f (x + y) = f x + f y
<VAR>R : Type u_1<VAR>S : Type u_6<VAR>M : Type u_9<VAR>M₃ : Type u_12<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module S M₃<VAR>σ : R →+* S<VAR>f : M →ₛₗ[σ] M₃<GOAL>f 0 = 0
<VAR>R : Type u_1<VAR>S : Type u_6<VAR>M : Type u_9<VAR>M₃ : Type u_12<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module S M₃<VAR>σ : R →+* S<VAR>f : M →ₛₗ[σ] M₃<VAR>c : R<VAR>x : M<GOAL>f (c • x) = σ c • f x
<VAR>R : Type u_1<VAR>M : Type u_9<VAR>M₂ : Type u_11<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>fₗ : M →ₗ[R] M₂<VAR>c : R<VAR>x : M<GOAL>fₗ (c • x) = c • fₗ x
<VAR>R : Type u_1<VAR>S : Type u_6<VAR>M : Type u_9<VAR>M₃ : Type u_12<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module S M₃<VAR>σ : R →+* S<VAR>f : M →ₛₗ[σ] M₃<VAR>σ' : S →+* R<VAR>RingHomInvPair σ σ'<VAR>c : S<VAR>x : M<GOAL>c • f x = f (σ' c • x)
<VAR>R : Type u_1<VAR>S : Type u_6<VAR>M : Type u_9<VAR>M₃ : Type u_12<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module S M₃<VAR>σ : R →+* S<VAR>f : M →ₛₗ[σ] M₃<VAR>h : Function.Injective ⇑f<VAR>x : M<GOAL>f x = 0 ↔ x = 0
<VAR>M : Type u_9<VAR>M₂ : Type u_11<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>R : Type u_17<VAR>S : Type u_18<VAR>Semiring S<VAR>SMul R M<VAR>Module S M<VAR>SMul R M₂<VAR>Module S M₂<VAR>self : LinearMap.CompatibleSMul M M₂ R S<VAR>fₗ : M →ₗ[S] M₂<VAR>c : R<VAR>x : M<GOAL>fₗ (c • x) = c • fₗ x
<VAR>M : Type u_9<VAR>M₂ : Type u_11<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>R : Type u_17<VAR>S : Type u_18<VAR>Semiring S<VAR>SMul R M<VAR>Module S M<VAR>SMul R M₂<VAR>Module S M₂<VAR>LinearMap.CompatibleSMul M M₂ R S<VAR>fₗ : M →ₗ[S] M₂<VAR>c : R<VAR>x : M<GOAL>fₗ (c • x) = c • fₗ x
<VAR>M : Type u_9<VAR>M₂ : Type u_11<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>R : Type u_17<VAR>S : Type u_18<VAR>Semiring S<VAR>SMul R M<VAR>Module S M<VAR>SMul R M₂<VAR>Module S M₂<VAR>SMul R S<VAR>LinearMap.CompatibleSMul M M₂ R S<VAR>IsScalarTower R S M₂<VAR>f : M →ₗ[S] M₂<VAR>hf : Function.Injective ⇑f<GOAL>IsScalarTower R S M
<VAR>R : Type u_1<VAR>S : Type u_6<VAR>M : Type u_9<VAR>M₂ : Type u_11<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>Module S M<VAR>Module S M₂<VAR>LinearMap.CompatibleSMul M M₂ R S<VAR>f : M →ₗ[S] M₂<GOAL>IsLinearMap R ⇑f
<VAR>R : Type u_1<VAR>S : Type u_6<VAR>M : Type u_9<VAR>M₃ : Type u_12<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module S M₃<VAR>σ : R →+* S<VAR>f : M →ₛₗ[σ] M₃<GOAL>⇑f.toAddMonoidHom = ⇑f
<VAR>R : Type u_1<VAR>S : Type u_6<VAR>M : Type u_9<VAR>M₂ : Type u_11<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>Module S M<VAR>Module S M₂<VAR>LinearMap.CompatibleSMul M M₂ R S<VAR>f : M →ₗ[S] M₂<GOAL>⇑(↑R f) = ⇑f
<VAR>R : Type u_1<VAR>S : Type u_6<VAR>M : Type u_9<VAR>M₂ : Type u_11<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>Module S M<VAR>Module S M₂<VAR>LinearMap.CompatibleSMul M M₂ R S<VAR>fₗ : M →ₗ[S] M₂<VAR>x : M<GOAL>(↑R fₗ) x = fₗ x
<VAR>R : Type u_1<VAR>S : Type u_6<VAR>M : Type u_9<VAR>M₂ : Type u_11<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>Module S M<VAR>Module S M₂<VAR>LinearMap.CompatibleSMul M M₂ R S<GOAL>Function.Injective ↑R
<VAR>R : Type u_1<VAR>S : Type u_6<VAR>M : Type u_9<VAR>M₂ : Type u_11<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>Module S M<VAR>Module S M₂<VAR>LinearMap.CompatibleSMul M M₂ R S<VAR>fₗ gₗ : M →ₗ[S] M₂<GOAL>↑R fₗ = ↑R gₗ ↔ fₗ = gₗ
<VAR>R : Type u_1<VAR>S : Type u_6<VAR>M : Type u_9<VAR>M₃ : Type u_12<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module S M₃<VAR>σ : R →+* S<GOAL>Function.Injective LinearMap.toAddMonoidHom
<VAR>R : Type u_1<VAR>S : Type u_6<VAR>M₃ : Type u_12<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M₃<VAR>Module S M₃<VAR>σ : R →+* S<VAR>f g : R →ₛₗ[σ] M₃<VAR>h : f 1 = g 1<GOAL>f = g
<VAR>R : Type u_1<VAR>M : Type u_9<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>σ : R →+* R<VAR>f g : R →ₛₗ[σ] M<GOAL>f = g ↔ f 1 = g 1
<VAR>R : Type u_1<VAR>S : Type u_6<VAR>M₃ : Type u_12<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M₃<VAR>Module S M₃<VAR>σ : Rᵐᵒᵖ →+* S<VAR>f g : R →ₛₗ[σ] M₃<VAR>h : f 1 = g 1<GOAL>f = g
<VAR>R : Type u_1<VAR>S : Type u_6<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<GOAL>∀ (a : R), f.toSemilinearMap a = (↑↑f).toFun a
<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M₁ : Type u_10<VAR>M₂ : Type u_11<VAR>M₃ : Type u_12<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring R₃<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>module_M₁ : Module R₁ M₁<VAR>module_M₂ : Module R₂ M₂<VAR>module_M₃ : Module R₃ M₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>f : M₂ →ₛₗ[σ₂₃] M₃<VAR>g : M₁ →ₛₗ[σ₁₂] M₂<VAR>x : M₁<GOAL>(f.comp g) x = f (g x)
<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M₁ : Type u_10<VAR>M₂ : Type u_11<VAR>M₃ : Type u_12<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring R₃<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>module_M₁ : Module R₁ M₁<VAR>module_M₂ : Module R₂ M₂<VAR>module_M₃ : Module R₃ M₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>f : M₂ →ₛₗ[σ₂₃] M₃<VAR>g : M₁ →ₛₗ[σ₁₂] M₂<GOAL>⇑(f.comp g) = ⇑f ∘ ⇑g
<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M₂ : Type u_11<VAR>M₃ : Type u_12<VAR>Semiring R₂<VAR>Semiring R₃<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>module_M₂ : Module R₂ M₂<VAR>module_M₃ : Module R₃ M₃<VAR>σ₂₃ : R₂ →+* R₃<VAR>f : M₂ →ₛₗ[σ₂₃] M₃<GOAL>f.comp LinearMap.id = f
<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M₂ : Type u_11<VAR>M₃ : Type u_12<VAR>Semiring R₂<VAR>Semiring R₃<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>module_M₂ : Module R₂ M₂<VAR>module_M₃ : Module R₃ M₃<VAR>σ₂₃ : R₂ →+* R₃<VAR>f : M₂ →ₛₗ[σ₂₃] M₃<GOAL>LinearMap.id.comp f = f
<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M₁ : Type u_10<VAR>M₂ : Type u_11<VAR>M₃ : Type u_12<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring R₃<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>module_M₁ : Module R₁ M₁<VAR>module_M₂ : Module R₂ M₂<VAR>module_M₃ : Module R₃ M₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>R₄ : Type u_17<VAR>M₄ : Type u_18<VAR>Semiring R₄<VAR>AddCommMonoid M₄<VAR>Module R₄ M₄<VAR>σ₃₄ : R₃ →+* R₄<VAR>σ₂₄ : R₂ →+* R₄<VAR>σ₁₄ : R₁ →+* R₄<VAR>RingHomCompTriple σ₂₃ σ₃₄ σ₂₄<VAR>RingHomCompTriple σ₁₃ σ₃₄ σ₁₄<VAR>RingHomCompTriple σ₁₂ σ₂₄ σ₁₄<VAR>f : M₁ →ₛₗ[σ₁₂] M₂<VAR>g : M₂ →ₛₗ[σ₂₃] M₃<VAR>h : M₃ →ₛₗ[σ₃₄] M₄<GOAL>(h.comp g).comp f = h.comp (g.comp f)
<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M₁ : Type u_10<VAR>M₂ : Type u_11<VAR>M₃ : Type u_12<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring R₃<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>module_M₁ : Module R₁ M₁<VAR>module_M₂ : Module R₂ M₂<VAR>module_M₃ : Module R₃ M₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>g : M₁ →ₛₗ[σ₁₂] M₂<VAR>hg : Function.Surjective ⇑g<GOAL>Function.Injective fun f => f.comp g
<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M₁ : Type u_10<VAR>M₂ : Type u_11<VAR>M₃ : Type u_12<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring R₃<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>module_M₁ : Module R₁ M₁<VAR>module_M₂ : Module R₂ M₂<VAR>module_M₃ : Module R₃ M₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>f : M₂ →ₛₗ[σ₂₃] M₃<VAR>g : M₁ →ₛₗ[σ₁₂] M₂<VAR>f' : M₂ →ₛₗ[σ₂₃] M₃<VAR>hg : Function.Surjective ⇑g<GOAL>f.comp g = f'.comp g ↔ f = f'
<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M₁ : Type u_10<VAR>M₂ : Type u_11<VAR>M₃ : Type u_12<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring R₃<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>module_M₁ : Module R₁ M₁<VAR>module_M₂ : Module R₂ M₂<VAR>module_M₃ : Module R₃ M₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>f : M₂ →ₛₗ[σ₂₃] M₃<VAR>hf : Function.Injective ⇑f<GOAL>Function.Injective fun g => f.comp g
<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M₁ : Type u_10<VAR>M₂ : Type u_11<VAR>M₃ : Type u_12<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring R₃<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>module_M₁ : Module R₁ M₁<VAR>module_M₂ : Module R₂ M₂<VAR>module_M₃ : Module R₃ M₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>f : M₂ →ₛₗ[σ₂₃] M₃<VAR>g g' : M₁ →ₛₗ[σ₁₂] M₂<VAR>hf : Function.Injective ⇑f<GOAL>f.comp g = f.comp g' ↔ g = g'
<VAR>R : Type u_1<VAR>S : Type u_6<VAR>M : Type u_9<VAR>M₂ : Type u_11<VAR>Semiring R<VAR>Semiring S<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>module_M : Module R M<VAR>module_M₂ : Module S M₂<VAR>σ : R →+* S<VAR>f : M →ₛₗ[σ] M₂<VAR>x : M<GOAL>f (-x) = -f x
<VAR>R : Type u_1<VAR>S : Type u_6<VAR>M : Type u_9<VAR>M₂ : Type u_11<VAR>Semiring R<VAR>Semiring S<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>module_M : Module R M<VAR>module_M₂ : Module S M₂<VAR>σ : R →+* S<VAR>f : M →ₛₗ[σ] M₂<VAR>x y : M<GOAL>f (x - y) = f x - f y
<VAR>R : Type u_17<VAR>S : Type u_18<VAR>Semiring R<VAR>Semiring S<VAR>g : R →+* S<VAR>a : R<GOAL>(Module.compHom.toLinearMap g) a = g a
<VAR>R : Type u_1<VAR>S : Type u_6<VAR>M : Type u_9<VAR>M₂ : Type u_11<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Semiring R<VAR>Module R M<VAR>Semiring S<VAR>Module S M₂<VAR>σ : R →+* S<VAR>f : M →ₑ+[↑σ] M₂<GOAL>⇑↑f = ⇑f
<VAR>R : Type u_1<VAR>S : Type u_6<VAR>M : Type u_9<VAR>M₂ : Type u_11<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Semiring R<VAR>Module R M<VAR>Semiring S<VAR>Module S M₂<VAR>σ : R →+* S<VAR>f g : M →ₑ+[↑σ] M₂<VAR>h : ↑f = ↑g<GOAL>f = g
<VAR>R : Type u_1<VAR>M : Type u_9<VAR>M₂ : Type u_11<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>f : M → M₂<VAR>lin : IsLinearMap R f<VAR>x : M<GOAL>(IsLinearMap.mk' f lin) x = f x
<VAR>R : Type u_17<VAR>M : Type u_18<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>c : R<GOAL>IsLinearMap R fun z => c • z
<VAR>R : Type u_17<VAR>M : Type u_18<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>a : M<GOAL>IsLinearMap R fun c => c • a
<VAR>R : Type u_1<VAR>M : Type u_9<VAR>M₂ : Type u_11<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>f : M → M₂<VAR>lin : IsLinearMap R f<GOAL>f 0 = 0
<VAR>R : Type u_1<VAR>M : Type u_9<VAR>Semiring R<VAR>AddCommGroup M<VAR>Module R M<GOAL>IsLinearMap R fun z => -z
<VAR>R : Type u_1<VAR>M : Type u_9<VAR>M₂ : Type u_11<VAR>Semiring R<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>Module R M<VAR>Module R M₂<VAR>f : M → M₂<VAR>lin : IsLinearMap R f<VAR>x : M<GOAL>f (-x) = -f x
<VAR>R : Type u_1<VAR>M : Type u_9<VAR>M₂ : Type u_11<VAR>Semiring R<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>Module R M<VAR>Module R M₂<VAR>f : M → M₂<VAR>lin : IsLinearMap R f<VAR>x y : M<GOAL>f (x - y) = f x - f y
<VAR>M : Type u_9<VAR>M₂ : Type u_11<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<GOAL>Function.Injective AddMonoidHom.toNatLinearMap
<VAR>M : Type u_9<VAR>M₂ : Type u_11<VAR>AddCommGroup M<VAR>AddCommGroup M₂<GOAL>Function.Injective AddMonoidHom.toIntLinearMap
<VAR>M : Type u_9<VAR>M₂ : Type u_11<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>f : M →+ M₂<GOAL>⇑f.toIntLinearMap = ⇑f
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>S : Type u_6<VAR>M : Type u_9<VAR>M₂ : Type u_11<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>Monoid S<VAR>DistribMulAction S M₂<VAR>SMulCommClass R₂ S M₂<VAR>a : S<VAR>f : M →ₛₗ[σ₁₂] M₂<VAR>x : M<GOAL>(a • f) x = a • f x
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>S : Type u_6<VAR>M : Type u_9<VAR>M₂ : Type u_11<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>Monoid S<VAR>DistribMulAction S M₂<VAR>SMulCommClass R₂ S M₂<VAR>a : S<VAR>f : M →ₛₗ[σ₁₂] M₂<GOAL>⇑(a • f) = a • ⇑f
<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>M : Type u_9<VAR>M₂ : Type u_11<VAR>Semiring R₁<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R₁ M<VAR>Module R₂ M₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>x : M<GOAL>0 x = 0
<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_9<VAR>M₂ : Type u_11<VAR>M₃ : Type u_12<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring R₃<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R₁ M<VAR>Module R₂ M₂<VAR>Module R₃ M₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>g : M₂ →ₛₗ[σ₂₃] M₃<GOAL>g.comp 0 = 0
<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_9<VAR>M₂ : Type u_11<VAR>M₃ : Type u_12<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring R₃<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R₁ M<VAR>Module R₂ M₂<VAR>Module R₃ M₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>f : M →ₛₗ[σ₁₂] M₂<GOAL>LinearMap.comp 0 f = 0
<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>M : Type u_9<VAR>M₂ : Type u_11<VAR>Semiring R₁<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R₁ M<VAR>Module R₂ M₂<VAR>σ₁₂ : R₁ →+* R₂<GOAL>default = 0
<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>M : Type u_9<VAR>M₂ : Type u_11<VAR>Semiring R₁<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R₁ M<VAR>Module R₂ M₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>f g : M →ₛₗ[σ₁₂] M₂<VAR>x : M<GOAL>(f + g) x = f x + g x
<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_9<VAR>M₂ : Type u_11<VAR>M₃ : Type u_12<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring R₃<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R₁ M<VAR>Module R₂ M₂<VAR>Module R₃ M₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>f : M →ₛₗ[σ₁₂] M₂<VAR>g h : M₂ →ₛₗ[σ₂₃] M₃<GOAL>(h + g).comp f = h.comp f + g.comp f
<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_9<VAR>M₂ : Type u_11<VAR>M₃ : Type u_12<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring R₃<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R₁ M<VAR>Module R₂ M₂<VAR>Module R₃ M₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>f g : M →ₛₗ[σ₁₂] M₂<VAR>h : M₂ →ₛₗ[σ₂₃] M₃<GOAL>h.comp (f + g) = h.comp f + h.comp g
<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>M : Type u_9<VAR>N₂ : Type u_14<VAR>Semiring R₁<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommGroup N₂<VAR>Module R₁ M<VAR>Module R₂ N₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>f : M →ₛₗ[σ₁₂] N₂<VAR>x : M<GOAL>(-f) x = -f x
<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_9<VAR>M₂ : Type u_11<VAR>N₃ : Type u_15<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring R₃<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommGroup N₃<VAR>Module R₁ M<VAR>Module R₂ M₂<VAR>Module R₃ N₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>f : M →ₛₗ[σ₁₂] M₂<VAR>g : M₂ →ₛₗ[σ₂₃] N₃<GOAL>(-g).comp f = -g.comp f
<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_9<VAR>N₂ : Type u_14<VAR>N₃ : Type u_15<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring R₃<VAR>AddCommMonoid M<VAR>AddCommGroup N₂<VAR>AddCommGroup N₃<VAR>Module R₁ M<VAR>Module R₂ N₂<VAR>Module R₃ N₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>f : M →ₛₗ[σ₁₂] N₂<VAR>g : N₂ →ₛₗ[σ₂₃] N₃<GOAL>g.comp (-f) = -g.comp f
<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>M : Type u_9<VAR>N₂ : Type u_14<VAR>Semiring R₁<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommGroup N₂<VAR>Module R₁ M<VAR>Module R₂ N₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>f g : M →ₛₗ[σ₁₂] N₂<VAR>x : M<GOAL>(f - g) x = f x - g x
<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_9<VAR>M₂ : Type u_11<VAR>N₃ : Type u_15<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring R₃<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommGroup N₃<VAR>Module R₁ M<VAR>Module R₂ M₂<VAR>Module R₃ N₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>f : M →ₛₗ[σ₁₂] M₂<VAR>g h : M₂ →ₛₗ[σ₂₃] N₃<GOAL>(g - h).comp f = g.comp f - h.comp f
<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_9<VAR>N₂ : Type u_14<VAR>N₃ : Type u_15<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring R₃<VAR>AddCommMonoid M<VAR>AddCommGroup N₂<VAR>AddCommGroup N₃<VAR>Module R₁ M<VAR>Module R₂ N₂<VAR>Module R₃ N₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>f g : M →ₛₗ[σ₁₂] N₂<VAR>h : N₂ →ₛₗ[σ₂₃] N₃<GOAL>h.comp (g - f) = h.comp g - h.comp f
<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>M : Type u_9<VAR>M₂ : Type u_11<VAR>Semiring R₁<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R₁ M<VAR>Module R₂ M₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>a : M<VAR>f : M →ₛₗ[σ₁₂] M₂<GOAL>(LinearMap.evalAddMonoidHom a) f = f a
<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>M : Type u_9<VAR>M₂ : Type u_11<VAR>Semiring R₁<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R₁ M<VAR>Module R₂ M₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>f : M →ₛₗ[σ₁₂] M₂<GOAL>LinearMap.toAddMonoidHom' f = f.toAddMonoidHom
<VAR>R₁ : Type u_2<VAR>M : Type u_9<VAR>Semiring R₁<VAR>AddCommMonoid M<VAR>Module R₁ M<VAR>Subsingleton M<GOAL>LinearMap.id = 0
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>S₃ : Type u_7<VAR>M : Type u_9<VAR>M₂ : Type u_11<VAR>M₃ : Type u_12<VAR>Semiring R<VAR>Semiring R₂<VAR>Semiring R₃<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module R₂ M₂<VAR>Module R₃ M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>Monoid S₃<VAR>DistribMulAction S₃ M₃<VAR>SMulCommClass R₃ S₃ M₃<VAR>a : S₃<VAR>g : M₂ →ₛₗ[σ₂₃] M₃<VAR>f : M →ₛₗ[σ₁₂] M₂<GOAL>(a • g).comp f = a • g.comp f
<VAR>R : Type u_1<VAR>S : Type u_6<VAR>M : Type u_9<VAR>M₂ : Type u_11<VAR>M₃ : Type u_12<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Monoid S<VAR>DistribMulAction S M₂<VAR>Module R M₂<VAR>Module R M₃<VAR>SMulCommClass R S M₂<VAR>DistribMulAction S M₃<VAR>SMulCommClass R S M₃<VAR>LinearMap.CompatibleSMul M₃ M₂ S R<VAR>g : M₃ →ₗ[R] M₂<VAR>a : S<VAR>f : M →ₗ[R] M₃<GOAL>g ∘ₗ (a • f) = a • g ∘ₗ f
<VAR>R : Type u_17<VAR>S : Type u_18<VAR>M : Type u_19<VAR>N : Type u_20<VAR>Semiring R<VAR>Semiring S<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Module S M<VAR>Module S N<VAR>LinearMap.CompatibleSMul M N R S<GOAL>↑R 0 = 0
<VAR>R : Type u_17<VAR>S : Type u_18<VAR>M : Type u_19<VAR>N : Type u_20<VAR>Semiring R<VAR>Semiring S<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Module S M<VAR>Module S N<VAR>LinearMap.CompatibleSMul M N R S<VAR>f g : M →ₗ[S] N<GOAL>↑R (f + g) = ↑R f + ↑R g
<VAR>R : Type u_17<VAR>S : Type u_18<VAR>M : Type u_19<VAR>N : Type u_20<VAR>Semiring R<VAR>Semiring S<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Module S M<VAR>Module S N<VAR>LinearMap.CompatibleSMul M N R S<VAR>f : M →ₗ[S] N<GOAL>↑R (-f) = -↑R f
<VAR>R : Type u_17<VAR>S : Type u_18<VAR>M : Type u_19<VAR>N : Type u_20<VAR>Semiring R<VAR>Semiring S<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Module S M<VAR>Module S N<VAR>LinearMap.CompatibleSMul M N R S<VAR>R₁ : Type u_21<VAR>Semiring R₁<VAR>Module R₁ N<VAR>SMulCommClass S R₁ N<VAR>SMulCommClass R R₁ N<VAR>c : R₁<VAR>f : M →ₗ[S] N<GOAL>↑R (c • f) = c • ↑R f
<VAR>R : Type u_17<VAR>S : Type u_18<VAR>M : Type u_19<VAR>N : Type u_20<VAR>Semiring R<VAR>Semiring S<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Module S M<VAR>Module S N<VAR>LinearMap.CompatibleSMul M N R S<VAR>R₁ : Type u_21<VAR>Semiring R₁<VAR>Module R₁ N<VAR>SMulCommClass S R₁ N<VAR>SMulCommClass R R₁ N<VAR>fₗ : M →ₗ[S] N<GOAL>(LinearMap.restrictScalarsₗ N) fₗ = ↑R fₗ
<VAR>A : Type u_1<VAR>Mul A<VAR>self : IsJordan A<VAR>a b : A<GOAL>a * a * (a * b) = a * (a * a * b)
<VAR>A : Type u_1<VAR>Mul A<VAR>self : IsJordan A<VAR>a b : A<GOAL>a * b * a = a * (b * a)
<VAR>A : Type u_1<VAR>Mul A<VAR>self : IsJordan A<VAR>a b : A<GOAL>b * a * (a * a) = b * (a * a) * a
<VAR>A : Type u_1<VAR>Mul A<VAR>self : IsJordan A<VAR>a b : A<GOAL>a * a * (b * a) = a * a * b * a
<VAR>A : Type u_1<VAR>Mul A<VAR>self : IsJordan A<VAR>a b : A<GOAL>a * b * (a * a) = a * (b * (a * a))
<VAR>A : Type u_1<VAR>CommMagma A<VAR>self : IsCommJordan A<VAR>a b : A<GOAL>a * b * (a * a) = a * (b * (a * a))
<VAR>A : Type u_1<VAR>NonUnitalNonAssocRing A<VAR>IsJordan A<VAR>a : A<GOAL>Commute (L a) (R a)
<VAR>A : Type u_1<VAR>NonUnitalNonAssocRing A<VAR>IsJordan A<VAR>a : A<GOAL>Commute (L a) (L (a * a))
<VAR>A : Type u_1<VAR>NonUnitalNonAssocRing A<VAR>IsJordan A<VAR>a : A<GOAL>Commute (L a) (R (a * a))
<VAR>A : Type u_1<VAR>NonUnitalNonAssocRing A<VAR>IsJordan A<VAR>a : A<GOAL>Commute (L (a * a)) (R a)
<VAR>A : Type u_1<VAR>NonUnitalNonAssocRing A<VAR>IsJordan A<VAR>a : A<GOAL>Commute (R a) (R (a * a))
<VAR>A : Type u_1<VAR>NonUnitalNonAssocCommRing A<VAR>IsCommJordan A<VAR>a b : A<GOAL>2 • (⁅L a, L (a * b)⁆ + ⁅L b, L (b * a)⁆) = ⁅L (a * a), L b⁆ + ⁅L (b * b), L a⁆
<VAR>A : Type u_1<VAR>NonUnitalNonAssocCommRing A<VAR>a b c : A<GOAL>⁅L (a + b + c), L ((a + b + c) * (a + b + c))⁆ = ⁅L a + L b + L c, L (a * a) + L (b * b) + L (c * c) + 2 • L (a * b) + 2 • L (c * a) + 2 • L (b * c)⁆
<VAR>A : Type u_1<VAR>NonUnitalNonAssocCommRing A<VAR>a b c : A<GOAL>⁅L a + L b + L c, L (a * a) + L (b * b) + L (c * c) + 2 • L (a * b) + 2 • L (c * a) + 2 • L (b * c)⁆ = ⁅L a, L (a * a)⁆ + ⁅L a, L (b * b)⁆ + ⁅L a, L (c * c)⁆ + ⁅L a, 2 • L (a * b)⁆ + ⁅L a, 2 • L (c * a)⁆ + ⁅L a, 2 • L (b * c)⁆ + (⁅L b, L (a * a)⁆ + ⁅L b, L (b * b)⁆ + ⁅L b, L (c * c)⁆ + ⁅L b, 2 • L (a * b)⁆ + ⁅L b, 2 • L (c * a)⁆ + ⁅L b, 2 • L (b * c)⁆) + (⁅L c, L (a * a)⁆ + ⁅L c, L (b * b)⁆ + ⁅L c, L (c * c)⁆ + ⁅L c, 2 • L (a * b)⁆ + ⁅L c, 2 • L (c * a)⁆ + ⁅L c, 2 • L (b * c)⁆)