Theorems · Theorem · group theory
Nat.card_zpowers
∀ {α : Type u_3} [inst : Group α] (a : α), Nat.card ↥(Subgroup.zpowers a) = orderOf aSee also Fintype.card_zpowers.
- Defined in
- Mathlib.Data.ZMod.QuotientGroup
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 95 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Group
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
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
- Groupstatement and proof · cited by 6,238
- Subgroupstatement · cited by 3,593
- ZModproof · cited by 1,024
- Nat.cardstatement and proof · cited by 844
- orderOfstatement · cited by 324
- Subgroup.zpowersstatement and proof · cited by 204
- Nat.card_congrproof · cited by 133
- MulAction.orbitproof · cited by 114
- Function.minimalPeriodproof · cited by 100
- Nat.card_zmodproof · cited by 13
Cited by13
Results whose statement or proof uses this declaration.
- orderOf_eq_card_of_forall_mem_zpowersproof · cited by 13
- IsCyclic.exists_ofOrder_eq_natCardproof · cited by 3
- isCyclic_iff_exists_orderOf_eq_natCardproof · cited by 3
- NumberField.IsCMField.zpowers_complexConj_eq_topproof · cited by 1
- IsPrimitiveRoot.card_rootsOfUnity'proof · cited by 1
- Monoid.le_minOrder_iff_forall_subgroupproof · cited by 1
- IsCyclic.card_powMonoidHom_rangeproof · cited by 1
- exists_pow_ne_one_of_isCyclicproof · cited by 1
- card_dvd_exponent_pow_rankproof · cited by 1
- IsPGroup.powEquiv_symm_applyproof · cited by 0
- NumberField.IsCMField.of_forall_isConjproof · cited by 0
- IsCyclotomicExtension.Rat.galEquivZMod_stabilizerproof · cited by 0