Theorems · Theorem · group theory
AddSubgroup.mem_zmultiples_iff
∀ {G : Type u_1} [inst : AddGroup G] {g h : G}, h ∈ AddSubgroup.zmultiples g ↔ ∃ k, k • g = h- Cited by
- 11 results in Mathlib
- Foundations
- Depth 33 from the axioms · uses propext
- Assumes
- AddGroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
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 · cited by 3,232
- AddSubgroup.zmultiplesstatement · cited by 493
Cited by11
Results whose statement or proof uses this declaration.
- isAddCyclic_iff_exists_zmultiples_eq_topproof · cited by 4
- AddSubgroup.zmultiples_eq_zmultiples_iffproof · cited by 3
- addMonoidHomOfForallMemZMultiples_apply_genproof · cited by 2
- AddSubgroup.zsmul_mem_zmultiplesproof · cited by 2
- AddSubgroup.zsmul_mem_zmultiples_iff_exists_sub_divproof · cited by 2
- addOrderOf_dvd_of_mem_zmultiplesproof · cited by 1
- mem_zmultiples_zsmul_iffproof · cited by 1
- IsOfFinAddOrder.of_mem_zmultiplesproof · cited by 1
- AddMonoidHom.eq_iff_eq_on_generatorproof · cited by 1
- AddSubgroup.le_zmultiples_iffproof · cited by 0
- AddSubgroup.intCast_mem_zmultiples_oneproof · cited by 0