Theorems · Theorem · number theory
FiniteField.forall_pow_eq_one_iff
∀ (K : Type u_1) [inst : Field K] [inst_1 : Fintype K] (i : ℕ), (∀ (x : Kˣ), x ^ i = 1) ↔ Fintype.card K - 1 ∣ i
- Defined in
- Mathlib.FieldTheory.Finite.Basic
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 139 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
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
- Fieldstatement and proof · cited by 7,404
- Unitsstatement and proof · cited by 2,804
- mul_commproof · cited by 2,262
- Fintype.cardstatement · cited by 1,386
- one_powproof · cited by 521
- pow_mulproof · cited by 210
- Subgroup.zpowersproof · cited by 204
- Nat.card_eq_fintype_cardproof · cited by 200
- orderOf_dvd_iff_pow_eq_oneproof · cited by 22
- IsCyclic.exists_generatorproof · cited by 14
- orderOf_eq_card_of_forall_mem_zpowersproof · cited by 13
Cited by1
Results whose statement or proof uses this declaration.
- FiniteField.sum_pow_unitsproof · cited by 1