Theorems · Definition · group theory
MonoidHom.id
(M : Type u_10) → [inst : MulOne M] → M →* M
The identity map from a monoid to itself.
- Defined in
- Mathlib.Algebra.Group.Hom.Defs
- Cited by
- 323 results in Mathlib
- Foundations
- Depth 5 from the axioms, rests on 21 definitions · uses no axioms
- Assumes
- MulOne
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 by424
Results whose statement or proof uses this declaration.
- LinearMap.idproof · cited by 625
- NonUnitalAlgHomClassproof · cited by 75
- Algebra.lmulproof · cited by 41
- NonUnitalStarAlgHom.compproof · cited by 40
- MonoidHom.id_applystatement and proof · cited by 33
- NonUnitalStarAlgHomClass.toNonUnitalStarAlgHomproof · cited by 23
- Monoid.Coprod.sndproof · cited by 15
- Monoid.Coprod.fstproof · cited by 15
- Unitization.inrNonUnitalStarAlgHomproof · cited by 13
- NonUnitalSubalgebra.inclusionstatement · cited by 12
- NonUnitalStarAlgHom.idproof · cited by 12
- NonUnitalStarSubalgebra.inclusionproof · cited by 12
Showing the 200 most cited of 424.