exists_sq_eq_two_iff — Mathlib

English

For prime p ≠ 2, IsSquare(2 mod p) holds iff p ≡ 1 or 7 modulo 8.

Русский

Для p ≠ 2: IsSquare(2 mod p) тогда и только тогда, когда p ≡ 1 или 7 (mod 8).

LaTeX

$$$IsSquare(2\bmod p) \iff p \equiv 1 \text{ or } 7 \pmod{8}$$$

Lean4

/-- `2` is a square modulo an odd prime `p` iff `p` is congruent to `1` or `7` mod `8`. -/
theorem exists_sq_eq_two_iff (hp : p ≠ 2) : IsSquare (2 : ZMod p) ↔ p % 8 = 1 ∨ p % 8 = 7 :=
  by
  rw [FiniteField.isSquare_two_iff, card p]
  have h₁ := (Prime.mod_two_eq_one_iff_ne_two Fact.out).mpr hp
  cutsat

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