Theorems · Inductive type · group theory
MonoidHom
(M : Type u_10) → (N : Type u_11) → [MulOne M] → [MulOne N] → Type (max u_10 u_11)
M →* N is the type of functions M → N that preserve the MulOne structure.
MonoidHom is used for both monoid and group homomorphisms.
When possible, instead of parametrizing results over (f : M →* N),
you should parametrize over (F : Type*) [MonoidHomClass F M N] (f : F).
When you extend this structure, make sure to extend MonoidHomClass.
[Wikidata Q868169](https://www.wikidata.org/wiki/Q868169)
- Defined in
- Mathlib.Algebra.Group.Hom.Defs
- Cited by
- 3,629 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 2 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MulOnestatement · cited by 65
Cited by4,686
Results whose statement or proof uses this declaration.
- RingHomClass.toRingHomproof · cited by 746
- MonoidHom.compstatement and proof · cited by 469
- Representationproof · cited by 396
- MonoidHom.idstatement · cited by 323
- MonoidHom.rangestatement and proof · cited by 314
- Subgroup.mapstatement and proof · cited by 301
- MonoidHomClass.toMonoidHomstatement · cited by 294
- Rep.resstatement and proof · cited by 213
- MonoidHom.kerstatement and proof · cited by 212
- MonoidWithZeroHom.ofClassproof · cited by 204
- Subgroup.subtypestatement · cited by 185
- Algebra.normstatement · cited by 155
Showing the 200 most cited of 4,686.