Theorems · Theorem · group theory

MulSemiringActionHom.mk.inj

∀ {M : Type u_1} {inst : Monoid M} {N : Type u_2} {inst_1 : Monoid N} {φ : M →* N} {R : Type u_10} {inst_2 : Semiring R}
  {inst_3 : MulSemiringAction M R} {S : Type u_12} {inst_4 : Semiring S} {inst_5 : MulSemiringAction N S}
  {toDistribMulActionHom : R →ₑ+[φ] S} {map_one' : toDistribMulActionHom.toFun 1 = 1}
  {map_mul' :
    ∀ (x y : R), toDistribMulActionHom.toFun (x * y) = toDistribMulActionHom.toFun x * toDistribMulActionHom.toFun y}
  {toDistribMulActionHom_1 : R →ₑ+[φ] S} {map_one'_1 : toDistribMulActionHom_1.toFun 1 = 1}
  {map_mul'_1 :
    ∀ (x y : R),
      toDistribMulActionHom_1.toFun (x * y) = toDistribMulActionHom_1.toFun x * toDistribMulActionHom_1.toFun y},
  { toDistribMulActionHom := toDistribMulActionHom, map_one' := map_one', map_mul' := map_mul' } =
      { toDistribMulActionHom := toDistribMulActionHom_1, map_one' := map_one'_1, map_mul' := map_mul'_1 } →
    toDistribMulActionHom = toDistribMulActionHom_1

Defined in

Mathlib.GroupTheory.GroupAction.Hom

Cited by

1 results in Mathlib

Foundations

Depth 18 from the axioms · uses no axioms