Mathlib Map

Theorems · Theorem · group theory

MulHom.mk.congr_simp

∀ {M : Type u_10} {N : Type u_11} [inst : Mul M] [inst_1 : Mul N] (toFun toFun_1 : M → N) (e_toFun : toFun = toFun_1)
  (map_mul' : ∀ (x y : M), toFun (x * y) = toFun x * toFun y),
  { toFun := toFun, map_mul' := map_mul' } = { toFun := toFun_1, map_mul' := ⋯ }
Defined in
Mathlib.Algebra.Group.UniqueProds.Basic
Cited by
1 results in Mathlib
Foundations
Depth 5 from the axioms · uses no axioms
Assumes
MulMul
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

FreeSemigroup.toFreeMonoid_mk_eq_cons · cited by 1FreeSemigroup.toFreeMonoi…MulHom · cited by 299MulHommk.congr_simpCITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • MulHomstatement · cited by 299

Cited by1

Results whose statement or proof uses this declaration.