Theorems · Definition · group theory
AddHom.id
(M : Type u_10) → [inst : Add M] → M →ₙ+ M
The identity map from a type with addition to itself.
- Defined in
- Mathlib.Algebra.Group.Hom.Defs
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
- Assumes
- Add
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.
- AddHomstatement · cited by 294
Cited by18
Results whose statement or proof uses this declaration.
- AddHom.id_applystatement and proof · cited by 4
- Module.length_eq_of_surjectiveproof · cited by 4
- AddHom.toAddEquivstatement and proof · cited by 2
- WithZero.mapAddHom_idstatement and proof · cited by 1
- Ring.coe_jacobson_quotientproof · cited by 1
- AddMonoidAlgebra.mapDomainNonUnitalRingHom_idstatement and proof · cited by 0
- AddHom.id_compstatement · cited by 0
- AddHom.toAddEquiv_applystatement and proof · cited by 0
- AddHom.toAddEquiv_symm_applystatement and proof · cited by 0
- AddSemigrp.hom_idstatement · cited by 0
- isNoetherian_of_finite_isArtinianproof · cited by 0
- AddSemigrp.ofHom_idstatement · cited by 0