English
In a finite field of odd characteristic, for nonzero a, a^{|F|/2} equals either 1 or -1.
Русский
В конечном поле с нечетной характеристикой для ненулевого a выполняется либо a^{|F|/2}=1, либо a^{|F|/2}=-1.
LaTeX
$$$\\\\forall F \\\\text{finite}, \\\\text{ringChar}(F) \\\\ne 2 \\\\Rightarrow \\\\forall a \\\\ne 0, \\\\exists b \\\\in \\\\{1,-1\\\\}: a^{|F|/2} = b$$$
Lean4
/-- If `F` has odd characteristic, then for nonzero `a : F`, we have that `a ^ (#F / 2) = ±1`. -/
theorem pow_dichotomy (hF : ringChar F ≠ 2) {a : F} (ha : a ≠ 0) :
a ^ (Fintype.card F / 2) = 1 ∨ a ^ (Fintype.card F / 2) = -1 :=
by
have h₁ := FiniteField.pow_card_sub_one_eq_one a ha
rw [← Nat.two_mul_odd_div_two (FiniteField.odd_card_of_char_ne_two hF), mul_comm, pow_mul, pow_two] at h₁
exact mul_self_eq_one_iff.mp h₁
