English
For a finite field K of size q, and any i ∈ ℕ, every unit x ∈ K^× satisfies x^i = 1 if and only if (q − 1) divides i.
Русский
Для конечного поля K размера q и любого i ∈ ℕ все единицы удовлетворяют x^i = 1 тогда и только тогда, когда (q−1) делится на i.
LaTeX
$$$(\forall x \in K^{\times}, x^i = 1) \iff (q - 1) \\mid i$$$
Lean4
theorem forall_pow_eq_one_iff (i : ℕ) : (∀ x : Kˣ, x ^ i = 1) ↔ q - 1 ∣ i := by
classical
obtain ⟨x, hx⟩ := IsCyclic.exists_generator (α := Kˣ)
rw [← Nat.card_eq_fintype_card, ← Nat.card_units, ← orderOf_eq_card_of_forall_mem_zpowers hx,
orderOf_dvd_iff_pow_eq_one]
constructor
· intro h; apply h
· intro h y
simp_rw [← mem_powers_iff_mem_zpowers] at hx
rcases hx y with ⟨j, rfl⟩
rw [← pow_mul, mul_comm, pow_mul, h, one_pow]
