Theorems · Theorem · group theory
Nat.card_zmultiples
∀ {α : Type u_3} [inst : AddGroup α] (a : α), Nat.card ↥(AddSubgroup.zmultiples a) = addOrderOf aSee also Fintype.card_zmultiples.
- Defined in
- Mathlib.Data.ZMod.QuotientGroup
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 95 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.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setproof · cited by 53,352
- Set.Elemproof · cited by 7,166
- AddGroupstatement and proof · cited by 4,410
- AddSubgroupstatement · cited by 3,232
- HVAdd.hVAddproof · cited by 1,820
- ZModproof · cited by 1,024
- Nat.cardstatement and proof · cited by 844
- AddSubgroup.zmultiplesstatement and proof · cited by 493
- addOrderOfstatement · cited by 208
- Nat.card_congrproof · cited by 133
- Function.minimalPeriodproof · cited by 100
- AddAction.orbitproof · cited by 86
Cited by11
Results whose statement or proof uses this declaration.
- addOrderOf_eq_card_of_forall_mem_zmultiplesproof · cited by 8
- finite_zmultiplesproof · cited by 3
- AddMonoid.le_minOrder_iff_forall_addSubgroupproof · cited by 2
- isAddCyclic_iff_exists_addOrderOf_eq_natCardproof · cited by 2
- IsAddCyclic.exists_ofOrder_eq_natCardproof · cited by 1
- AddCircle.isAddFundamentalDomain_of_ae_ballproof · cited by 1
- AddCircle.volume_of_add_preimage_eqproof · cited by 1
- ZMod.minOrderproof · cited by 1
- card_dvd_exponent_nsmul_rankproof · cited by 1
- IsAddCyclic.card_nsmulAddMonoidHom_rangeproof · cited by 1
- exists_nsmul_ne_zero_of_isAddCyclicproof · cited by 0