English
Let F be a finite field with characteristic not equal to 2. For every nonzero a in F, a is a square in F if and only if a^{|F|/2} = 1.
Русский
Пусть F — конечное поле с характеристикой, не равной 2. Для каждого ненулевого a ∈ F верно: a является квадратом в F тогда и только тогда a^{|F|/2} = 1.
LaTeX
$$$\forall a \in F^{\times}: IsSquare(a) \iff a^{\lvert F \rvert / 2} = 1$$$
Lean4
/-- A non-zero `a : F` is a square if and only if `a ^ (#F / 2) = 1`. -/
theorem isSquare_iff (hF : ringChar F ≠ 2) {a : F} (ha : a ≠ 0) : IsSquare a ↔ a ^ (Fintype.card F / 2) = 1 :=
by
apply (iff_congr _ (by simp [Units.ext_iff])).mp (FiniteField.unit_isSquare_iff hF (Units.mk0 a ha))
simp only [IsSquare, Units.ext_iff, Units.val_mk0, Units.val_mul]
constructor
· rintro ⟨y, hy⟩; exact ⟨y, hy⟩
· rintro ⟨y, rfl⟩
have hy : y ≠ 0 := by rintro rfl; simp at ha
refine ⟨Units.mk0 y hy, ?_⟩; simp
