Theorems · Theorem · group theory
AddMonoidHom.map_zero
∀ {M : Type u_4} {N : Type u_5} [inst : AddZero M] [inst_1 : AddZero N] (f : M →+ N), f 0 = 0If f is an additive monoid homomorphism then f 0 = 0.
- Defined in
- Mathlib.Algebra.Group.Hom.Defs
- Cited by
- 47 results in Mathlib
- Foundations
- Depth 11 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- AddMonoidHomstatement and proof · cited by 3,230
- AddZerostatement and proof · cited by 87
- AddMonoidHom.toZeroHomproof · cited by 61
- ZeroHom.map_zero'proof · cited by 7
Cited by47
Results whose statement or proof uses this declaration.
- lie_zeroproof · cited by 18
- zero_lieproof · cited by 16
- AddMonoidHom.ker_eq_bot_iffproof · cited by 14
- CategoryTheory.AddMonObj.comp_zeroproof · cited by 6
- FreeAddMonoid.hom_eqproof · cited by 6
- addOrderOf_injectiveproof · cited by 5
- Finsupp.liftAddHom_apply_singleproof · cited by 5
- AddMonoidHom.map_finsum_of_injectiveproof · cited by 4
- AddMonoidHom.map_finsum_pliftproof · cited by 3
- Submodule.norm_eq_iInf_iff_inner_eq_zeroproof · cited by 2
- CategoryTheory.pullbackShiftFunctorZero_inv_appproof · cited by 2
- AddMonoidHom.isOfFinAddOrderproof · cited by 2