Theorems · Inductive type · group theory
AddMonoidHomClass
(F : Type u_10) → (M : outParam (Type u_11)) → (N : outParam (Type u_12)) → [AddZero M] → [AddZero N] → [FunLike F M N] → Prop
AddMonoidHomClass F M N states that F is a type of AddZero-preserving
homomorphisms.
You should also extend this typeclass when you extend AddMonoidHom.
- Defined in
- Mathlib.Algebra.Group.Hom.Defs
- Cited by
- 252 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 by283
Results whose statement or proof uses this declaration.
- map_substatement and proof · cited by 565
- map_sumstatement and proof · cited by 455
- map_negstatement and proof · cited by 378
- AddMonoidHomClass.toAddMonoidHomstatement and proof · cited by 232
- AddSubmonoid.mapstatement and proof · cited by 99
- AddSubmonoid.comapstatement and proof · cited by 62
- injective_iff_map_eq_zerostatement and proof · cited by 62
- AddMonoidHom.mrangestatement and proof · cited by 61
- map_finsuppSumstatement and proof · cited by 43
- map_nsmulstatement and proof · cited by 41
- HasSum.mapstatement and proof · cited by 32
- map_list_sumstatement and proof · cited by 31
Showing the 200 most cited of 283.