English
Let F be a finite field of odd characteristic. Then a unit a ∈ F^× is a square in F if and only if a^{|F|/2} = 1.
Русский
Пусть F — конечное поле нечетной характеристики. Тогда элемент a ∈ F^× является квадратом в F тогда и только тогда, когда a^{|F|/2} = 1.
LaTeX
$$$\text{IsSquare}(a) \iff a^{|F|/2} = 1 \quad (\text{char}(F) \neq 2)$$$
Lean4
/-- A unit `a` of a finite field `F` of odd characteristic is a square
if and only if `a ^ (#F / 2) = 1`. -/
theorem unit_isSquare_iff (hF : ringChar F ≠ 2) (a : Fˣ) : IsSquare a ↔ a ^ (Fintype.card F / 2) = 1 := by
classical
obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := Fˣ)
obtain ⟨n, hn⟩ : a ∈ Submonoid.powers g := by rw [mem_powers_iff_mem_zpowers]; apply hg
have hodd := Nat.two_mul_odd_div_two (FiniteField.odd_card_of_char_ne_two hF)
constructor
· rintro ⟨y, rfl⟩
rw [← pow_two, ← pow_mul, hodd]
apply_fun Units.val using Units.val_injective
push_cast
exact FiniteField.pow_card_sub_one_eq_one (y : F) (Units.ne_zero y)
· subst a; intro h
rw [← Nat.card_eq_fintype_card] at hodd h
have key : 2 * (Nat.card F / 2) ∣ n * (Nat.card F / 2) :=
by
rw [← pow_mul] at h
rw [hodd, ← Nat.card_units, ← orderOf_eq_card_of_forall_mem_zpowers hg]
apply orderOf_dvd_of_pow_eq_one h
have : 0 < Nat.card F / 2 := Nat.div_pos Finite.one_lt_card (by simp)
obtain ⟨m, rfl⟩ := Nat.dvd_of_mul_dvd_mul_right this key
refine ⟨g ^ m, ?_⟩
dsimp
rw [mul_comm, pow_mul, pow_two]
