Theorems · Theorem · group theory
orderOf_dvd_card
∀ {G : Type u_1} [inst : Group G] [inst_1 : Fintype G] {x : G}, orderOf x ∣ Fintype.card G- Defined in
- Mathlib.GroupTheory.OrderOfElement
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Fintypestatement and proof · cited by 7,736
- Groupstatement and proof · cited by 6,238
- HasQuotient.Quotientproof · cited by 2,301
- mul_commproof · cited by 2,262
- Fintype.cardstatement and proof · cited by 1,386
- orderOfstatement · cited by 324
- Subgroup.zpowersproof · cited by 204
- Fintype.card_congrproof · cited by 67
- Fintype.card_prodproof · cited by 19
- Fintype.card_zpowersproof · cited by 5
- Subgroup.groupEquivQuotientProdSubgroupproof · cited by 4
Cited by9
Results whose statement or proof uses this declaration.
- Nat.totient_evenproof · cited by 4
- Equiv.Perm.alternatingGroup_le_of_isPreprimitive_of_isThreeCycle_memproof · cited by 2
- Equiv.Perm.subgroup_eq_top_of_isPreprimitive_of_isSwap_memproof · cited by 1
- MonoidHom.independent_range_of_coprime_orderproof · cited by 1
- Group.exponent_dvd_cardproof · cited by 1
- Ideal.IsPrincipal.of_isPrincipal_pow_of_coprimeproof · cited by 0
- zpow_mod_cardproof · cited by 0
- pow_mod_cardproof · cited by 0
- FractionalIdeal.isPrincipal.of_isPrincipal_pow_of_coprimeproof · cited by 0