exists_sq_eq_neg_one_iff — Mathlib

English

For a prime p, −1 is a quadratic residue mod p if and only if p ≡ 1 (mod 4).

Русский

Для простого p ∶ −1 является квадратичным вычетом по модулю p тогда и только тогда, когда p ≡ 1 (mod 4).

LaTeX

$$$(-1) \\text{ is a square modulo } p \\Leftrightarrow p \equiv 1 \\pmod{4}$$$

Lean4

/-- `-1` is a square in `ZMod p` iff `p` is not congruent to `3` mod `4`. -/
theorem exists_sq_eq_neg_one_iff : IsSquare (-1 : ZMod p) ↔ p % 4 ≠ 3 := by
  rw [FiniteField.isSquare_neg_one_iff, card p]

Похожие утверждения