ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>SMulCommClass R A A<VAR>IsScalarTower R A A<GOAL>LinearMap.mulLeft R 0 = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>SMulCommClass R A A<VAR>IsScalarTower R A A<GOAL>LinearMap.mulRight R 0 = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>Module R A<VAR>SMulCommClass R A A<VAR>IsScalarTower R A A<GOAL>⇑(NonUnitalAlgHom.lmul R A) = ⇑(LinearMap.mul R A)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>Module R A<VAR>SMulCommClass R A A<VAR>IsScalarTower R A A<VAR>a b : A<GOAL>Commute (LinearMap.mulLeft R a) (LinearMap.mulRight R b)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>Module R A<VAR>SMulCommClass R A A<VAR>IsScalarTower R A A<VAR>a b : A<GOAL>LinearMap.mulLeft R (a * b) = LinearMap.mulLeft R a ∘ₗ LinearMap.mulLeft R b
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>NonUnitalSemiring A<VAR>Module R A<VAR>SMulCommClass R A A<VAR>IsScalarTower R A A<VAR>a b : A<GOAL>LinearMap.mulRight R (a * b) = LinearMap.mulRight R b ∘ₗ LinearMap.mulRight R a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →ₗ[R] B<GOAL>(∀ (x y : A), f (x * y) = f x * f y) ↔ (LinearMap.mul R A).compr₂ f = (LinearMap.mul R B ∘ₗ f).compl₂ f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>⇑(Algebra.lmul R A) = ⇑(LinearMap.mul R A)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>Function.Injective ⇑(Algebra.lmul R A)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>x : A<GOAL>IsUnit ((Algebra.lmul R A) x) ↔ IsUnit x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>a : A<GOAL>LinearMap.mulLeft R a = 0 ↔ a = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>a : A<GOAL>LinearMap.mulRight R a = 0 ↔ a = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>LinearMap.mulLeft R 1 = LinearMap.id
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>LinearMap.mulRight R 1 = LinearMap.id
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>a : A<VAR>n : ℕ<GOAL>LinearMap.mulLeft R a ^ n = LinearMap.mulLeft R (a ^ n)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>a : A<VAR>n : ℕ<GOAL>LinearMap.mulRight R a ^ n = LinearMap.mulRight R (a ^ n)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Ring A<VAR>Algebra R A<VAR>NoZeroDivisors A<VAR>x : A<VAR>hx : x ≠ 0<GOAL>Function.Injective ⇑(LinearMap.mulLeft R x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Ring A<VAR>Algebra R A<VAR>NoZeroDivisors A<VAR>x : A<VAR>hx : x ≠ 0<GOAL>Function.Injective ⇑(LinearMap.mulRight R x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Ring A<VAR>Algebra R A<VAR>NoZeroDivisors A<VAR>x : A<VAR>hx : x ≠ 0<GOAL>Function.Injective ⇑((LinearMap.mul R A) x)
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>Monoid M<VAR>Ring R<VAR>MulSemiringAction M R<VAR>a : M<VAR>S : Subring R<GOAL>a • S = Subring.map (MulSemiringAction.toRingHom M R a) S
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>Monoid M<VAR>Ring R<VAR>MulSemiringAction M R<VAR>m : M<VAR>S : Subring R<GOAL>↑(m • S) = m • ↑S
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>Monoid M<VAR>Ring R<VAR>MulSemiringAction M R<VAR>m : M<VAR>S : Subring R<GOAL>(m • S).toAddSubgroup = m • S.toAddSubgroup
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>Monoid M<VAR>Ring R<VAR>MulSemiringAction M R<VAR>m : M<VAR>S : Subring R<GOAL>(m • S).toSubsemiring = m • S.toSubsemiring
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>Monoid M<VAR>Ring R<VAR>MulSemiringAction M R<VAR>m : M<VAR>r : R<VAR>S : Subring R<GOAL>r ∈ S → m • r ∈ m • S
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>Monoid M<VAR>Ring R<VAR>MulSemiringAction M R<VAR>m : M<VAR>r : R<VAR>S : Subring R<GOAL>r ∈ m • S ↔ ∃ s ∈ S, m • s = r
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>Monoid M<VAR>Ring R<VAR>MulSemiringAction M R<VAR>a : M<GOAL>a • ⊥ = ⊥
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>Monoid M<VAR>Ring R<VAR>MulSemiringAction M R<VAR>a : M<VAR>S T : Subring R<GOAL>a • (S ⊔ T) = a • S ⊔ a • T
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>Monoid M<VAR>Ring R<VAR>MulSemiringAction M R<VAR>a : M<VAR>s : Set R<GOAL>a • Subring.closure s = Subring.closure (a • s)
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>Group M<VAR>Ring R<VAR>MulSemiringAction M R<VAR>a : M<VAR>S : Subring R<VAR>x : R<GOAL>a • x ∈ a • S ↔ x ∈ S
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>Group M<VAR>Ring R<VAR>MulSemiringAction M R<VAR>a : M<VAR>S : Subring R<VAR>x : R<GOAL>x ∈ a • S ↔ a⁻¹ • x ∈ S
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>Group M<VAR>Ring R<VAR>MulSemiringAction M R<VAR>a : M<VAR>S : Subring R<VAR>x : R<GOAL>x ∈ a⁻¹ • S ↔ a • x ∈ S
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>Group M<VAR>Ring R<VAR>MulSemiringAction M R<VAR>a : M<VAR>S T : Subring R<GOAL>a • S ≤ a • T ↔ S ≤ T
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>Group M<VAR>Ring R<VAR>MulSemiringAction M R<VAR>a : M<VAR>S T : Subring R<GOAL>a • S ≤ T ↔ S ≤ a⁻¹ • T
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>Group M<VAR>Ring R<VAR>MulSemiringAction M R<VAR>a : M<VAR>S T : Subring R<GOAL>S ≤ a • T ↔ a⁻¹ • S ≤ T
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>GroupWithZero M<VAR>Ring R<VAR>MulSemiringAction M R<VAR>a : M<VAR>ha : a ≠ 0<VAR>S : Subring R<VAR>x : R<GOAL>a • x ∈ a • S ↔ x ∈ S
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>GroupWithZero M<VAR>Ring R<VAR>MulSemiringAction M R<VAR>a : M<VAR>ha : a ≠ 0<VAR>S : Subring R<VAR>x : R<GOAL>x ∈ a • S ↔ a⁻¹ • x ∈ S
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>GroupWithZero M<VAR>Ring R<VAR>MulSemiringAction M R<VAR>a : M<VAR>ha : a ≠ 0<VAR>S : Subring R<VAR>x : R<GOAL>x ∈ a⁻¹ • S ↔ a • x ∈ S
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>GroupWithZero M<VAR>Ring R<VAR>MulSemiringAction M R<VAR>a : M<VAR>ha : a ≠ 0<VAR>S T : Subring R<GOAL>a • S ≤ a • T ↔ S ≤ T
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>GroupWithZero M<VAR>Ring R<VAR>MulSemiringAction M R<VAR>a : M<VAR>ha : a ≠ 0<VAR>S T : Subring R<GOAL>a • S ≤ T ↔ S ≤ a⁻¹ • T
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>GroupWithZero M<VAR>Ring R<VAR>MulSemiringAction M R<VAR>a : M<VAR>ha : a ≠ 0<VAR>S T : Subring R<GOAL>S ≤ a • T ↔ a⁻¹ • S ≤ T
<VAR>M : Type u_1<VAR>Mul M<VAR>Std.IdempotentOp fun x x_1 => x * x_1<VAR>a : M<GOAL>IsIdempotentElem a
<VAR>M : Type u_1<VAR>Mul M<VAR>p : M<VAR>h : IsIdempotentElem p<GOAL>p * p = p
<VAR>S : Type u_3<VAR>Semigroup S<VAR>p q : S<VAR>h : Commute p q<VAR>h₁ : IsIdempotentElem p<VAR>h₂ : IsIdempotentElem q<GOAL>IsIdempotentElem (p * q)
<VAR>M₀ : Type u_4<VAR>MulZeroClass M₀<GOAL>IsIdempotentElem 0
<VAR>M₁ : Type u_5<VAR>MulOneClass M₁<GOAL>IsIdempotentElem 1
<VAR>R : Type u_6<VAR>NonAssocRing R<VAR>p : R<VAR>h : IsIdempotentElem p<GOAL>IsIdempotentElem (1 - p)
<VAR>R : Type u_6<VAR>NonAssocRing R<VAR>p : R<GOAL>IsIdempotentElem (1 - p) ↔ IsIdempotentElem p
<VAR>N : Type u_2<VAR>Monoid N<VAR>p : N<VAR>n : ℕ<VAR>h : IsIdempotentElem p<GOAL>IsIdempotentElem (p ^ n)
<VAR>N : Type u_2<VAR>Monoid N<VAR>p : N<VAR>n : ℕ<VAR>h : IsIdempotentElem p<GOAL>p ^ (n + 1) = p
<VAR>G : Type u_7<VAR>Group G<VAR>p : G<GOAL>IsIdempotentElem p ↔ p = 1
<VAR>G₀ : Type u_8<VAR>CancelMonoidWithZero G₀<VAR>p : G₀<GOAL>IsIdempotentElem p ↔ p = 0 ∨ p = 1
<VAR>M₀ : Type u_4<VAR>MulZeroClass M₀<GOAL>↑0 = 0
<VAR>M₁ : Type u_5<VAR>MulOneClass M₁<GOAL>↑1 = 1
<VAR>R : Type u_6<VAR>NonAssocRing R<VAR>p : { p // IsIdempotentElem p }<GOAL>↑pᶜ = 1 - ↑p
<VAR>R : Type u_6<VAR>NonAssocRing R<VAR>p : { p // IsIdempotentElem p }<GOAL>pᶜᶜ = p
<VAR>R : Type u_6<VAR>NonAssocRing R<GOAL>0ᶜ = 1
<VAR>R : Type u_6<VAR>NonAssocRing R<GOAL>1ᶜ = 0
<VAR>R : Type x<VAR>Distrib R<VAR>a x y x' y' : R<VAR>h : SemiconjBy a x y<VAR>h' : SemiconjBy a x' y'<GOAL>SemiconjBy a (x + x') (y + y')
<VAR>R : Type x<VAR>Distrib R<VAR>a b x y : R<VAR>ha : SemiconjBy a x y<VAR>hb : SemiconjBy b x y<GOAL>SemiconjBy (a + b) x y
<VAR>R : Type x<VAR>Mul R<VAR>HasDistribNeg R<VAR>a x y : R<VAR>h : SemiconjBy a x y<GOAL>SemiconjBy a (-x) (-y)
<VAR>R : Type x<VAR>Mul R<VAR>HasDistribNeg R<VAR>a x y : R<GOAL>SemiconjBy a (-x) (-y) ↔ SemiconjBy a x y
<VAR>R : Type x<VAR>Mul R<VAR>HasDistribNeg R<VAR>a x y : R<VAR>h : SemiconjBy a x y<GOAL>SemiconjBy (-a) x y
<VAR>R : Type x<VAR>Mul R<VAR>HasDistribNeg R<VAR>a x y : R<GOAL>SemiconjBy (-a) x y ↔ SemiconjBy a x y
<VAR>R : Type x<VAR>MulOneClass R<VAR>HasDistribNeg R<VAR>a : R<GOAL>SemiconjBy a (-1) (-1)
<VAR>R : Type x<VAR>MulOneClass R<VAR>HasDistribNeg R<VAR>x : R<GOAL>SemiconjBy (-1) x x
<VAR>R : Type x<VAR>NonUnitalNonAssocRing R<VAR>a x y x' y' : R<VAR>h : SemiconjBy a x y<VAR>h' : SemiconjBy a x' y'<GOAL>SemiconjBy a (x - x') (y - y')
<VAR>R : Type x<VAR>NonUnitalNonAssocRing R<VAR>a b x y : R<VAR>ha : SemiconjBy a x y<VAR>hb : SemiconjBy b x y<GOAL>SemiconjBy (a - b) x y
<VAR>R : Type u<VAR>S : Type u₁<VAR>Monoid R<VAR>Monoid S<VAR>φ : R →* S<VAR>A : Type v<VAR>B : Type w<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction S B<VAR>f : A →ₛₙₐ[φ] B<GOAL>f.toFun = ⇑f
<VAR>R : Type u<VAR>S : Type u₁<VAR>Monoid R<VAR>Monoid S<VAR>φ : R →* S<VAR>A : Type v<VAR>B : Type w<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction S B<VAR>F : Type u_2<VAR>FunLike F A B<VAR>NonUnitalAlgSemiHomClass F φ A B<VAR>f : F<GOAL>⇑↑f = ⇑f
<VAR>R : Type u<VAR>S : Type u₁<VAR>Monoid R<VAR>Monoid S<VAR>φ : R →* S<VAR>A : Type v<VAR>B : Type w<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction S B<GOAL>Function.Injective DFunLike.coe
<VAR>R : Type u<VAR>S : Type u₁<VAR>Monoid R<VAR>Monoid S<VAR>φ : R →* S<VAR>A : Type v<VAR>B : Type w<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction S B<VAR>f g : A →ₛₙₐ[φ] B<VAR>h : ∀ (x : A), f x = g x<GOAL>f = g
<VAR>R : Type u<VAR>S : Type u₁<VAR>Monoid R<VAR>Monoid S<VAR>φ : R →* S<VAR>A : Type v<VAR>B : Type w<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction S B<VAR>f g : A →ₛₙₐ[φ] B<GOAL>f = g ↔ ∀ (x : A), f x = g x
<VAR>R : Type u<VAR>S : Type u₁<VAR>Monoid R<VAR>Monoid S<VAR>φ : R →* S<VAR>A : Type v<VAR>B : Type w<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction S B<VAR>f g : A →ₛₙₐ[φ] B<VAR>h : f = g<VAR>x : A<GOAL>f x = g x
<VAR>R : Type u<VAR>S : Type u₁<VAR>Monoid R<VAR>Monoid S<VAR>φ : R →* S<VAR>A : Type v<VAR>B : Type w<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction S B<VAR>f : A → B<VAR>h₁ : ∀ (m : R) (x : A), f (m • x) = φ m • f x<VAR>h₂ : { toFun := f, map_smul' := h₁ }.toFun 0 = 0<VAR>h₃ : ∀ (x y : A), { toFun := f, map_smul' := h₁ }.toFun (x + y) = { toFun := f, map_smul' := h₁ }.toFun x + { toFun := f, map_smul' := h₁ }.toFun y<VAR>h₄ : ∀ (x y : A), { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun (x * y) = { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun x * { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun y<GOAL>⇑{ toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ } = f
<VAR>R : Type u<VAR>S : Type u₁<VAR>Monoid R<VAR>Monoid S<VAR>φ : R →* S<VAR>A : Type v<VAR>B : Type w<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction S B<VAR>f : A →ₛₙₐ[φ] B<VAR>h₁ : ∀ (m : R) (x : A), f (m • x) = φ m • f x<VAR>h₂ : { toFun := ⇑f, map_smul' := h₁ }.toFun 0 = 0<VAR>h₃ : ∀ (x y : A), { toFun := ⇑f, map_smul' := h₁ }.toFun (x + y) = { toFun := ⇑f, map_smul' := h₁ }.toFun x + { toFun := ⇑f, map_smul' := h₁ }.toFun y<VAR>h₄ : ∀ (x y : A), { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun (x * y) = { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun x * { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun y<GOAL>{ toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ } = f
<VAR>R : Type u<VAR>S : Type u₁<VAR>Monoid R<VAR>Monoid S<VAR>φ : R →* S<VAR>A : Type v<VAR>B : Type w<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction S B<VAR>f : A →ₛₙₐ[φ] B<GOAL>f.toDistribMulActionHom = ↑f
<VAR>R : Type u<VAR>S : Type u₁<VAR>Monoid R<VAR>Monoid S<VAR>φ : R →* S<VAR>A : Type v<VAR>B : Type w<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction S B<VAR>f : A →ₛₙₐ[φ] B<GOAL>f.toMulHom = ↑f
<VAR>R : Type u<VAR>S : Type u₁<VAR>Monoid R<VAR>Monoid S<VAR>φ : R →* S<VAR>A : Type v<VAR>B : Type w<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction S B<VAR>f : A →ₛₙₐ[φ] B<GOAL>⇑↑f = ⇑f
<VAR>R : Type u<VAR>S : Type u₁<VAR>Monoid R<VAR>Monoid S<VAR>φ : R →* S<VAR>A : Type v<VAR>B : Type w<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction S B<VAR>f g : A →ₛₙₐ[φ] B<VAR>h : ↑f = ↑g<GOAL>f = g
<VAR>R : Type u<VAR>S : Type u₁<VAR>Monoid R<VAR>Monoid S<VAR>φ : R →* S<VAR>A : Type v<VAR>B : Type w<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction S B<VAR>f : A →ₛₙₐ[φ] B<VAR>h₁ : ∀ (m : R) (x : A), f (m • x) = φ m • f x<VAR>h₂ : { toFun := ⇑f, map_smul' := h₁ }.toFun 0 = 0<VAR>h₃ : ∀ (x y : A), { toFun := ⇑f, map_smul' := h₁ }.toFun (x + y) = { toFun := ⇑f, map_smul' := h₁ }.toFun x + { toFun := ⇑f, map_smul' := h₁ }.toFun y<VAR>h₄ : ∀ (x y : A), { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun (x * y) = { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun x * { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun y<GOAL>↑{ toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ } = { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }
<VAR>R : Type u<VAR>S : Type u₁<VAR>Monoid R<VAR>Monoid S<VAR>φ : R →* S<VAR>A : Type v<VAR>B : Type w<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction S B<VAR>f : A →ₛₙₐ[φ] B<VAR>h₁ : ∀ (m : R) (x : A), f (m • x) = φ m • f x<VAR>h₂ : { toFun := ⇑f, map_smul' := h₁ }.toFun 0 = 0<VAR>h₃ : ∀ (x y : A), { toFun := ⇑f, map_smul' := h₁ }.toFun (x + y) = { toFun := ⇑f, map_smul' := h₁ }.toFun x + { toFun := ⇑f, map_smul' := h₁ }.toFun y<VAR>h₄ : ∀ (x y : A), { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun (x * y) = { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun x * { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun y<GOAL>↑{ toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ } = { toFun := ⇑f, map_mul' := h₄ }
<VAR>R : Type u<VAR>S : Type u₁<VAR>Monoid R<VAR>Monoid S<VAR>φ : R →* S<VAR>A : Type v<VAR>B : Type w<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction S B<VAR>f : A →ₛₙₐ[φ] B<VAR>c : R<VAR>x : A<GOAL>f (c • x) = φ c • f x
<VAR>R : Type u<VAR>S : Type u₁<VAR>Monoid R<VAR>Monoid S<VAR>φ : R →* S<VAR>A : Type v<VAR>B : Type w<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction S B<VAR>f : A →ₛₙₐ[φ] B<VAR>x y : A<GOAL>f (x + y) = f x + f y
<VAR>R : Type u<VAR>S : Type u₁<VAR>Monoid R<VAR>Monoid S<VAR>φ : R →* S<VAR>A : Type v<VAR>B : Type w<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction S B<VAR>f : A →ₛₙₐ[φ] B<VAR>x y : A<GOAL>f (x * y) = f x * f y
<VAR>R : Type u<VAR>S : Type u₁<VAR>Monoid R<VAR>Monoid S<VAR>φ : R →* S<VAR>A : Type v<VAR>B : Type w<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction S B<VAR>f : A →ₛₙₐ[φ] B<GOAL>f 0 = 0
<VAR>R : Type u<VAR>Monoid R<VAR>A : Type v<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<GOAL>⇑(NonUnitalAlgHom.id R A) = id
<VAR>R : Type u<VAR>S : Type u₁<VAR>Monoid R<VAR>Monoid S<VAR>φ : R →* S<VAR>A : Type v<VAR>B : Type w<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction S B<GOAL>⇑0 = 0
<VAR>R : Type u<VAR>Monoid R<VAR>A : Type v<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<GOAL>⇑1 = id
<VAR>R : Type u<VAR>S : Type u₁<VAR>Monoid R<VAR>Monoid S<VAR>φ : R →* S<VAR>A : Type v<VAR>B : Type w<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction S B<VAR>a : A<GOAL>0 a = 0
<VAR>R : Type u<VAR>Monoid R<VAR>A : Type v<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>a : A<GOAL>1 a = a
<VAR>R : Type u<VAR>S : Type u₁<VAR>T : Type u_1<VAR>Monoid R<VAR>Monoid S<VAR>Monoid T<VAR>φ : R →* S<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w₁<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction S B<VAR>NonUnitalNonAssocSemiring C<VAR>DistribMulAction T C<VAR>ψ : S →* T<VAR>χ : R →* T<VAR>f : B →ₛₙₐ[ψ] C<VAR>g : A →ₛₙₐ[φ] B<VAR>φ.CompTriple ψ χ<GOAL>⇑(f.comp g) = ⇑f ∘ ⇑g
<VAR>R : Type u<VAR>S : Type u₁<VAR>T : Type u_1<VAR>Monoid R<VAR>Monoid S<VAR>Monoid T<VAR>φ : R →* S<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w₁<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction S B<VAR>NonUnitalNonAssocSemiring C<VAR>DistribMulAction T C<VAR>ψ : S →* T<VAR>χ : R →* T<VAR>f : B →ₛₙₐ[ψ] C<VAR>g : A →ₛₙₐ[φ] B<VAR>φ.CompTriple ψ χ<VAR>x : A<GOAL>(f.comp g) x = f (g x)
<VAR>R : Type u<VAR>Monoid R<VAR>A : Type v<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>B₁ : Type u_2<VAR>NonUnitalNonAssocSemiring B₁<VAR>DistribMulAction R B₁<VAR>f : A →ₙₐ[R] B₁<VAR>g : B₁ → A<VAR>h₁ : Function.LeftInverse g ⇑f<VAR>h₂ : Function.RightInverse g ⇑f<GOAL>⇑(f.inverse g h₁ h₂) = g
<VAR>R : Type u<VAR>S : Type u₁<VAR>Monoid R<VAR>Monoid S<VAR>φ : R →* S<VAR>A : Type v<VAR>B : Type w<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction S B<VAR>φ' : S →* R<VAR>f : A →ₛₙₐ[φ] B<VAR>g : B → A<VAR>k : Function.RightInverse ⇑φ' ⇑φ<VAR>h₁ : Function.LeftInverse g ⇑f<VAR>h₂ : Function.RightInverse g ⇑f<GOAL>⇑(f.inverse' g k h₁ h₂) = g
<VAR>R : Type u<VAR>Monoid R<VAR>A : Type v<VAR>B : Type w<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction R B<VAR>self : A × B<GOAL>(NonUnitalAlgHom.fst R A B) self = self.1
<VAR>R : Type u<VAR>Monoid R<VAR>A : Type v<VAR>B : Type w<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction R B<VAR>self : A × B<GOAL>(NonUnitalAlgHom.snd R A B) self = self.2
<VAR>R : Type u<VAR>Monoid R<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w₁<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>NonUnitalNonAssocSemiring B<VAR>NonUnitalNonAssocSemiring C<VAR>DistribMulAction R B<VAR>DistribMulAction R C<VAR>f : A →ₙₐ[R] B<VAR>g : A →ₙₐ[R] C<VAR>i : A<GOAL>(f.prod g) i = Pi.prod (⇑f) (⇑g) i
<VAR>R : Type u<VAR>Monoid R<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w₁<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>NonUnitalNonAssocSemiring B<VAR>NonUnitalNonAssocSemiring C<VAR>DistribMulAction R B<VAR>DistribMulAction R C<VAR>f : A →ₙₐ[R] B<VAR>g : A →ₙₐ[R] C<GOAL>⇑(f.prod g) = Pi.prod ⇑f ⇑g
<VAR>R : Type u<VAR>Monoid R<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w₁<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>NonUnitalNonAssocSemiring B<VAR>NonUnitalNonAssocSemiring C<VAR>DistribMulAction R B<VAR>DistribMulAction R C<VAR>f : A →ₙₐ[R] B<VAR>g : A →ₙₐ[R] C<GOAL>(NonUnitalAlgHom.fst R B C).comp (f.prod g) = f
<VAR>R : Type u<VAR>Monoid R<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w₁<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>NonUnitalNonAssocSemiring B<VAR>NonUnitalNonAssocSemiring C<VAR>DistribMulAction R B<VAR>DistribMulAction R C<VAR>f : A →ₙₐ[R] B<VAR>g : A →ₙₐ[R] C<GOAL>(NonUnitalAlgHom.snd R B C).comp (f.prod g) = g
<VAR>R : Type u<VAR>Monoid R<VAR>A : Type v<VAR>B : Type w<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction R B<GOAL>(NonUnitalAlgHom.fst R A B).prod (NonUnitalAlgHom.snd R A B) = 1
<VAR>R : Type u<VAR>Monoid R<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w₁<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>NonUnitalNonAssocSemiring B<VAR>NonUnitalNonAssocSemiring C<VAR>DistribMulAction R B<VAR>DistribMulAction R C<VAR>f : (A →ₙₐ[R] B) × (A →ₙₐ[R] C)<GOAL>NonUnitalAlgHom.prodEquiv f = f.1.prod f.2
<VAR>R : Type u<VAR>Monoid R<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w₁<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>NonUnitalNonAssocSemiring B<VAR>NonUnitalNonAssocSemiring C<VAR>DistribMulAction R B<VAR>DistribMulAction R C<VAR>f : A →ₙₐ[R] B × C<GOAL>NonUnitalAlgHom.prodEquiv.symm f = ((NonUnitalAlgHom.fst R B C).comp f, (NonUnitalAlgHom.snd R B C).comp f)
<VAR>R : Type u<VAR>Monoid R<VAR>A : Type v<VAR>B : Type w<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction R B<GOAL>⇑(NonUnitalAlgHom.inl R A B) = fun x => (x, 0)
<VAR>R : Type u<VAR>Monoid R<VAR>A : Type v<VAR>B : Type w<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction R B<VAR>x : A<GOAL>(NonUnitalAlgHom.inl R A B) x = (x, 0)
<VAR>R : Type u<VAR>Monoid R<VAR>A : Type v<VAR>B : Type w<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction R B<GOAL>⇑(NonUnitalAlgHom.inr R A B) = Prod.mk 0
<VAR>R : Type u<VAR>Monoid R<VAR>A : Type v<VAR>B : Type w<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction R B<VAR>x : B<GOAL>(NonUnitalAlgHom.inr R A B) x = (0, x)
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>A : Type u_3<VAR>B : Type u_4<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →ₐ[R] B<GOAL>↑f = NonUnitalAlgHomClass.toNonUnitalAlgHom f
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>A : Type u_3<VAR>B : Type u_4<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →ₐ[R] B<GOAL>⇑↑f = ⇑f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>Monoid R<VAR>Monoid S<VAR>NonUnitalNonAssocSemiring A<VAR>NonUnitalNonAssocSemiring B<VAR>MulAction R S<VAR>DistribMulAction S A<VAR>DistribMulAction S B<VAR>DistribMulAction R A<VAR>DistribMulAction R B<VAR>IsScalarTower R S A<VAR>IsScalarTower R S B<VAR>f : A →ₙₐ[S] B<VAR>x : A<GOAL>(NonUnitalAlgHom.restrictScalars R f) x = f x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>Monoid R<VAR>Monoid S<VAR>NonUnitalNonAssocSemiring A<VAR>NonUnitalNonAssocSemiring B<VAR>MulAction R S<VAR>DistribMulAction S A<VAR>DistribMulAction S B<VAR>DistribMulAction R A<VAR>DistribMulAction R B<VAR>IsScalarTower R S A<VAR>IsScalarTower R S B<VAR>f : A →ₙₐ[S] B<GOAL>↑(NonUnitalAlgHom.restrictScalars R f) = ↑f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>Monoid R<VAR>Monoid S<VAR>NonUnitalNonAssocSemiring A<VAR>NonUnitalNonAssocSemiring B<VAR>MulAction R S<VAR>DistribMulAction S A<VAR>DistribMulAction S B<VAR>DistribMulAction R A<VAR>DistribMulAction R B<VAR>IsScalarTower R S A<VAR>IsScalarTower R S B<VAR>f : A →ₙₐ[S] B<GOAL>⇑(NonUnitalAlgHom.restrictScalars R f) = ⇑f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>Monoid R<VAR>Monoid S<VAR>NonUnitalNonAssocSemiring A<VAR>NonUnitalNonAssocSemiring B<VAR>MulAction R S<VAR>DistribMulAction S A<VAR>DistribMulAction S B<VAR>DistribMulAction R A<VAR>DistribMulAction R B<VAR>IsScalarTower R S A<VAR>IsScalarTower R S B<GOAL>Function.Injective (NonUnitalAlgHom.restrictScalars R)