Theorems · Inductive type · group theory
MonoidHomClass
(F : Type u_10) → (M : outParam (Type u_11)) → (N : outParam (Type u_12)) → [MulOne M] → [MulOne N] → [FunLike F M N] → Prop
MonoidHomClass F M N states that F is a type of Monoid-preserving homomorphisms.
You should also extend this typeclass when you extend MonoidHom.
- Defined in
- Mathlib.Algebra.Group.Hom.Defs
- Cited by
- 244 results in Mathlib
- Foundations
- Depth 3 from the axioms, rests on 5 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by289
Results whose statement or proof uses this declaration.
- map_powstatement and proof · cited by 503
- MonoidHomClass.toMonoidHomstatement and proof · cited by 294
- Submonoid.mapstatement and proof · cited by 190
- Submonoid.comapstatement and proof · cited by 179
- map_prodstatement and proof · cited by 108
- IsUnit.mapstatement and proof · cited by 104
- map_invstatement and proof · cited by 95
- MonoidHom.mrangestatement and proof · cited by 63
- map_list_prodstatement and proof · cited by 35
- MonoidHom.mkerstatement and proof · cited by 24
- Submonoid.le_comap_mapstatement and proof · cited by 24
- map_multiset_prodstatement and proof · cited by 21
Showing the 200 most cited of 289.