quadraticChar_eq_one_of_char_two — Mathlib

English

If the ring characteristic of F is 2, then χF(a) = 1 for every nonzero a.

Русский

Если характеристика кольца F равна 2, то χF(a) = 1 для любого ненулевого a.

LaTeX

$$$\text{If } \operatorname{ringChar}(F)=2:\;\forall a\in F^{\times},\; χ_F(a)=1$$$

Lean4

/-- If `ringChar F = 2`, then `quadraticChar F` takes the value `1` on nonzero elements. -/
theorem quadraticChar_eq_one_of_char_two (hF : ringChar F = 2) {a : F} (ha : a ≠ 0) : quadraticChar F a = 1 :=
  quadraticCharFun_eq_one_of_char_two hF ha

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