Theorems · Theorem · group theory
finite_zmultiples
∀ {α : Type u_3} [inst : AddGroup α] {a : α}, (↑(AddSubgroup.zmultiples a)).Finite ↔ IsOfFinAddOrder a- Defined in
- Mathlib.Data.ZMod.QuotientGroup
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- AddGroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- SetLike.coestatement and proof · cited by 8,199
- AddGroupstatement and proof · cited by 4,410
- AddSubgroupstatement · cited by 3,232
- Set.Finitestatement and proof · cited by 1,814
- AddSubgroup.zmultiplesstatement and proof · cited by 493
- IsOfFinAddOrderstatement · cited by 105
- Set.nonempty_coe_sortproof · cited by 23
- Set.finite_coe_iffproof · cited by 21
- Nat.card_zmultiplesproof · cited by 11
- addOrderOf_pos_iffproof · cited by 10
- Nat.card_pos_iffproof · cited by 6
- ZeroMemClass.coe_nonemptyproof · cited by 2
Cited by3
Results whose statement or proof uses this declaration.
- AddMonoid.le_minOrder_iff_forall_addSubgroupproof · cited by 2
- IsOfFinAddOrder.finite_zmultiplesproof · cited by 1
- infinite_zmultiplesproof · cited by 0