Theorems · Theorem · group theory
pow_card_eq_one
∀ {G : Type u_1} [inst : Group G] [inst_1 : Fintype G] {x : G}, x ^ Fintype.card G = 1- Defined in
- Mathlib.GroupTheory.OrderOfElement
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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
- Fintype.cardstatement · cited by 1,386
- Nat.card_eq_fintype_cardproof · cited by 200
- pow_card_eq_one'proof · cited by 9
Cited by9
Results whose statement or proof uses this declaration.
- FiniteField.pow_card_sub_one_eq_oneproof · cited by 7
- card_orderOf_eq_totient_aux₂proof · cited by 2
- MulChar.pow_card_eq_oneproof · cited by 2
- IsCyclic.card_pow_eq_one_leproof · cited by 2
- MulChar.apply_mem_rootsOfUnityproof · cited by 1
- ZMod.units_pow_card_sub_one_eq_oneproof · cited by 1
- ZMod.pow_totientproof · cited by 1
- IsCyclic.exists_apply_ne_oneproof · cited by 1
- Lagrange.nodal_subgroup_eq_X_pow_card_sub_oneproof · cited by 0