isSquare_two_iff — Mathlib

English

For odd primes p, 2 is a square modulo p iff p ≡ 1 or 7 mod 8.

Русский

Для простых p не равных 2, 2 является квадратом модulo 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 in `F` iff `#F` is not congruent to `3` or `5` mod `8`. -/
theorem isSquare_two_iff : IsSquare (2 : F) ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5 := by
  classical
  by_cases hF : ringChar F = 2
  · have h := FiniteField.even_card_of_char_two hF
    simp only [FiniteField.isSquare_of_char_two hF, true_iff]
    cutsat
  · have h := FiniteField.odd_card_of_char_ne_two hF
    rw [← quadraticChar_one_iff_isSquare (Ring.two_ne_zero hF), quadraticChar_two hF, χ₈_nat_eq_if_mod_eight]
    cutsat

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