Theorems · Theorem · group theory
MonoidHom.mk_coe
∀ {M : Type u_4} {N : Type u_5} [inst : MulOne M] [inst_1 : MulOne N] (f : M →* N)
(hmul : ∀ (x y : M), (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y), { toOneHom := ↑f, map_mul' := hmul } = f- Defined in
- Mathlib.Algebra.Group.Hom.Defs
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 12 from the axioms · uses Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MonoidHomstatement and proof · cited by 3,629
- OneHom.toFunstatement and proof · cited by 132
- MonoidHom.extproof · cited by 109
- MulOnestatement and proof · cited by 65
- OneHomClass.toOneHomstatement and proof · cited by 2
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.