quadraticChar_ne_one — Mathlib

English

If ringChar F ≠ 2, the quadratic character is not identically equal to 1.

Русский

Если ringChar F ≠ 2, квадратичный характер не тождественен единице.

LaTeX

$$$\operatorname{ringChar}(F) \neq 2 \Rightarrow χ_F \neq 1$$$

Lean4

/-- The quadratic character is nontrivial as a multiplicative character
when the domain has odd characteristic. -/
theorem quadraticChar_ne_one (hF : ringChar F ≠ 2) : quadraticChar F ≠ 1 :=
  by
  rcases quadraticChar_exists_neg_one' hF with ⟨a, ha⟩
  intro hχ
  simp only [hχ, one_apply a.isUnit, reduceCtorEq] at ha

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