isSquare_neg_two_iff — Mathlib

English

−2 is a square in F iff card(F) ≡ 3 or 5 mod 8 does not hold; equivalently card(F) mod 8 is not 5 or 7.

Русский

−2 — квадрат в F тогда и только тогда, когда карта поля по модулю 8 не равна 5 или 7.

LaTeX

$$$IsSquare(-2)\iff |F| \bmod 8 \neq 5 \wedge |F| \bmod 8 \neq 7$$$

Lean4

/-- `-2` is a square in `F` iff `#F` is not congruent to `5` or `7` mod `8`. -/
theorem isSquare_neg_two_iff : IsSquare (-2 : F) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7 := 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 (neg_ne_zero.mpr (Ring.two_ne_zero hF)), quadraticChar_neg_two hF,
      χ₈'_nat_eq_if_mod_eight]
    cutsat

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