English
An odd prime p is a square in ZMod-mod p iff a certain quadratic character not equal to −1 holds, equivalently IsSquare p.cast ↔ χ(p) ≠ −1.
Русский
Нечетный простейший p является квадратом в ZMod p тогда и только тогда, когда χ(p) ≠ −1.
LaTeX
$$$IsSquare(p\!\!\text{ cast}) \iff χ_{\text{mod p}}(...) ≠ -1$$$
Lean4
/-- An odd prime `p` is a square in `F` iff the quadratic character of `ZMod p` does not
take the value `-1` on `χ₄#F * #F`. -/
theorem isSquare_odd_prime_iff (hF : ringChar F ≠ 2) {p : ℕ} [Fact p.Prime] (hp : p ≠ 2) :
IsSquare (p : F) ↔ quadraticChar (ZMod p) (χ₄ (Fintype.card F) * Fintype.card F) ≠ -1 := by
classical
by_cases hFp : ringChar F = p
· rw [show (p : F) = 0 by rw [← hFp]; exact ringChar.Nat.cast_ringChar]
simp only [IsSquare.zero, Ne, true_iff, map_mul]
obtain ⟨n, _, hc⟩ := FiniteField.card F (ringChar F)
have hchar : ringChar F = ringChar (ZMod p) := by rw [hFp]; exact (ringChar_zmod_n p).symm
conv => enter [1, 1, 2]; rw [hc, Nat.cast_pow, map_pow, hchar, map_ringChar]
simp only [zero_pow n.ne_zero, mul_zero, zero_eq_neg, one_ne_zero, not_false_iff]
· rw [← Iff.not_left (@quadraticChar_neg_one_iff_not_isSquare F _ _ _ _), quadraticChar_odd_prime hF hp]
exact hFp
