quadraticChar_exists_neg_one — Mathlib

English

If the characteristic of F is odd, there exists an element a with χF(a) = −1.

Русский

Если характеристика поля F нечетная, существует элемент a such that χF(a) = −1.

LaTeX

$$$\text{If } \operatorname{char}(F)\neq 2:\;\exists a\in F,\; χ_F(a) = -1$$$

Lean4

/-- If `F` has odd characteristic, then `quadraticChar F` takes the value `-1`. -/
theorem quadraticChar_exists_neg_one (hF : ringChar F ≠ 2) : ∃ a, quadraticChar F a = -1 :=
  (FiniteField.exists_nonsquare hF).imp fun _ h₁ ↦ quadraticChar_neg_one_iff_not_isSquare.mpr h₁

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