Theorems · Theorem · group theory

MonoidHom.mk.congr_simp

∀ {M : Type u_10} {N : Type u_11} [inst : MulOne M] [inst_1 : MulOne N] (toOneHom toOneHom_1 : OneHom M N)
  (e_toOneHom : toOneHom = toOneHom_1)
  (map_mul' : ∀ (x y : M), toOneHom.toFun (x * y) = toOneHom.toFun x * toOneHom.toFun y),
  { toOneHom := toOneHom, map_mul' := map_mul' } = { toOneHom := toOneHom_1, map_mul' := ⋯ }

Defined in

Mathlib.Algebra.Group.Equiv.TypeTags

Cited by

21 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

MulOneMulOne