quadraticChar_one_iff_isSquare — Mathlib

English

If a ≠ 0, then χ(a) = 1 if and only if a is a square in F.

Русский

Если a ≠ 0, то χ(a) = 1 тогда и только тогда, когда a является квадратом в F.

LaTeX

$$$a\neq 0 \;\Rightarrow\; χ(a)=1 \iff \text{IsSquare}(a)$$$

Lean4

/-- For nonzero `a : F`, `quadraticChar F a = 1 ↔ IsSquare a`. -/
theorem quadraticChar_one_iff_isSquare {a : F} (ha : a ≠ 0) : quadraticChar F a = 1 ↔ IsSquare a := by
  simp only [quadraticChar_apply, quadraticCharFun, ha, if_false, ite_eq_left_iff, imp_false, not_not, reduceCtorEq]

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