Theorems · Theorem · nonassociative algebras

NonUnitalAlgHom.mk.inj

∀ {R : Type u} {S : Type u₁} {inst : Monoid R} {inst_1 : Monoid S} {φ : R →* S} {A : Type v} {B : Type w}
  {inst_2 : NonUnitalNonAssocSemiring A} {inst_3 : DistribMulAction R A} {inst_4 : NonUnitalNonAssocSemiring B}
  {inst_5 : DistribMulAction S B} {toDistribMulActionHom : A →ₑ+[φ] B}
  {map_mul' :
    ∀ (x y : A), toDistribMulActionHom.toFun (x * y) = toDistribMulActionHom.toFun x * toDistribMulActionHom.toFun y}
  {toDistribMulActionHom_1 : A →ₑ+[φ] B}
  {map_mul'_1 :
    ∀ (x y : A),
      toDistribMulActionHom_1.toFun (x * y) = toDistribMulActionHom_1.toFun x * toDistribMulActionHom_1.toFun y},
  { toDistribMulActionHom := toDistribMulActionHom, map_mul' := map_mul' } =
      { toDistribMulActionHom := toDistribMulActionHom_1, map_mul' := map_mul'_1 } →
    toDistribMulActionHom = toDistribMulActionHom_1

Defined in

Mathlib.Algebra.Algebra.NonUnitalHom

Cited by

1 results in Mathlib

Foundations

Depth 18 from the axioms · uses no axioms