quadraticCharFun_eq_one_of_char_two

English

If ringChar F = 2, then for any a ≠ 0, quadraticCharFun F a = 1.

Русский

Если характеристика кольца равна 2, то для любого a ≠ 0, quadCharFun F a = 1.

LaTeX

$$$(ringChar F) = 2 \Rightarrow (a \neq 0 \Rightarrow quadraticCharFun F a = 1)$$$

Lean4

/-- If `ringChar F = 2`, then `quadraticCharFun F` takes the value `1` on nonzero elements. -/
theorem quadraticCharFun_eq_one_of_char_two (hF : ringChar F = 2) {a : F} (ha : a ≠ 0) : quadraticCharFun F a = 1 :=
  by
  simp only [quadraticCharFun, ha, if_false, ite_eq_left_iff]
  exact fun h ↦ (h (FiniteField.isSquare_of_char_two hF a)).elim

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