Theorems · Theorem · group theory
injective_iff_map_eq_zero
∀ {F : Type u_7} {G : Type u_8} {H : Type u_9} [inst : AddGroup G] [inst_1 : AddZeroClass H] [inst_2 : FunLike F G H]
[AddMonoidHomClass F G H] (f : F), Function.Injective ⇑f ↔ ∀ (a : G), f a = 0 → a = 0A homomorphism from an additive group to an additive monoid is injective iff
its kernel is trivial. For the iff statement on the triviality of the kernel,
see injective_iff_map_eq_zero'.
- Defined in
- Mathlib.Algebra.Group.Hom.Basic
- Cited by
- 62 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- AddGroupstatement and proof · cited by 4,410
- FunLikestatement and proof · cited by 2,560
- map_zeroproof · cited by 1,614
- AddZeroClassstatement and proof · cited by 1,237
- map_addproof · cited by 964
- AddMonoidHomClassstatement and proof · cited by 252
- add_neg_cancelproof · cited by 213
- map_eq_zero_iffproof · cited by 62
- add_neg_eq_zeroproof · cited by 20
Cited by62
Results whose statement or proof uses this declaration.
- injective_iff_map_eq_zero'proof · cited by 11
- IsAlgebraic.exists_integral_multipleproof · cited by 8
- RingHom.ker_eq_bot_iff_eq_zeroproof · cited by 7
- algebraicIndependent_iffproof · cited by 6
- AddMonoidHom.injective_of_surjective_of_injective_of_injectiveproof · cited by 3
- IsIntegrallyClosed.pow_dvd_pow_iffproof · cited by 2
- FractionalIdeal.not_inv_le_one_of_ne_botproof · cited by 2
- ZMod.castHom_injectiveproof · cited by 2
- Algebra.IsAlgebraic.injective_tower_topproof · cited by 2
- ClassGroup.normBound_posproof · cited by 2
- ClassGroup.prod_finsetApprox_ne_zeroproof · cited by 2
- charpoly_leftMulMatrixproof · cited by 2