Theorems · Theorem · group theory
QuotientAddGroup.eq_zero_iff
∀ {G : Type u_1} [inst : AddGroup G] {N : AddSubgroup G} [inst_1 : N.Normal] (x : G), ↑x = 0 ↔ x ∈ N- Defined in
- Mathlib.GroupTheory.QuotientGroup.Defs
- Cited by
- 19 results in Mathlib
- Foundations
- Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- AddGroupAddSubgroup.Normal
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddGroupstatement and proof · cited by 4,410
- AddSubgroupstatement and proof · cited by 3,232
- add_zeroproof · cited by 2,707
- HasQuotient.Quotientstatement · cited by 2,301
- QuotientAddGroup.mkstatement · cited by 348
- AddSubgroup.Normalstatement and proof · cited by 183
- QuotientAddGroup.eqproof · cited by 24
- AddSubgroup.neg_mem_iffproof · cited by 5
Cited by19
Results whose statement or proof uses this declaration.
- QuotientAddGroup.ker_mk'proof · cited by 13
- AddCircle.coe_periodproof · cited by 5
- AddSubgroup.nsmul_index_memproof · cited by 3
- AddCircle.card_torsion_le_of_isSMulRegularproof · cited by 2
- AddCommGroup.isAddTorsion_quotient_range_nsmulAddMonoidHomproof · cited by 2
- CochainComplex.HomComplex.CohomologyClass.mk_eq_zero_iffproof · cited by 2
- QuotientAddGroup.norm_mkproof · cited by 2
- QuotientAddGroup.preimage_image_coeproof · cited by 1
- QuotientAddGroup.map_mk'_selfproof · cited by 1
- ProfiniteAddGrp.ProfiniteCompletion.mono_eta_iff_residuallyFiniteproof · cited by 1
- AddSubgroup.Normal.quotient_commutative_iff_addCommutator_leproof · cited by 1
- QuotientAddGroup.ker_le_range_iffproof · cited by 0