quadraticChar_neg_one_iff_not_isSquare

English

For any a in F, the quadratic character equals −1 precisely when a is not a square in F.

Русский

Для любого элемента a поля F квадратичный характер χF(a) равен −1 тогда, когда a не является квадратом в F.

LaTeX

$$$\forall F\ (\text{Field }F)\ (a:\,F),\quad χ_F(a) = -1 \iff \neg IsSquare(a)$$$

Lean4

/-- For `a : F`, `quadraticChar F a = -1 ↔ ¬ IsSquare a`. -/
theorem quadraticChar_neg_one_iff_not_isSquare {a : F} : quadraticChar F a = -1 ↔ ¬IsSquare a :=
  by
  by_cases ha : a = 0
  · simp only [ha, MulChar.map_zero, zero_eq_neg, one_ne_zero, IsSquare.zero, not_true]
  · rw [quadraticChar_eq_neg_one_iff_not_one ha, quadraticChar_one_iff_isSquare ha]

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