English
In a finite field, −1 is a square iff the field size is not congruent to 3 modulo 4.
Русский
В конечном поле −1 является квадратом тогда, когда размер поля не равен 3 по модулю 4.
LaTeX
$$$IsSquare(-1)\iff |F|\mod 4 \neq 3$$$
Lean4
/-- `-1` is a square in `F` iff `#F` is not congruent to `3` mod `4`. -/
theorem isSquare_neg_one_iff : IsSquare (-1 : F) ↔ Fintype.card F % 4 ≠ 3 := by
classical -- suggested by the linter (instead of `[DecidableEq F]`)
by_cases hF : ringChar F = 2
· simp only [FiniteField.isSquare_of_char_two hF, Ne, true_iff]
exact fun hf ↦ one_ne_zero <| (Nat.odd_of_mod_four_eq_three hf).symm.trans <| FiniteField.even_card_of_char_two hF
· have h₁ := FiniteField.odd_card_of_char_ne_two hF
rw [← quadraticChar_one_iff_isSquare (neg_ne_zero.mpr (one_ne_zero' F)), quadraticChar_neg_one hF,
χ₄_nat_eq_if_mod_four, h₁]
cutsat
