quadraticChar_exists_neg_one' — Mathlib

English

If F has odd characteristic, there exists a unit a in F such that χF(a) = −1.

Русский

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

LaTeX

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

Lean4

/-- If `F` has odd characteristic, then `quadraticChar F` takes the value `-1` on some unit. -/
theorem quadraticChar_exists_neg_one' (hF : ringChar F ≠ 2) : ∃ a : Fˣ, quadraticChar F a = -1 :=
  by
  refine (fun ⟨a, ha⟩ ↦ ⟨IsUnit.unit ?_, ha⟩) (quadraticChar_exists_neg_one hF)
  contrapose ha
  exact ne_of_eq_of_ne ((quadraticChar F).map_nonunit ha) (mt zero_eq_neg.mp one_ne_zero)

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