quadraticChar_two — Mathlib

English

For odd characteristic fields, χF(2) equals χ₈(|F|).

Русский

Для полей с нечетной характеристикой χF(2) равно χ₈(|F|).

LaTeX

$$$χ_F(2) = χ_8(|F|)$$$

Lean4

/-- The value of the quadratic character at `2` -/
theorem quadraticChar_two [DecidableEq F] (hF : ringChar F ≠ 2) : quadraticChar F 2 = χ₈ (Fintype.card F) :=
  IsQuadratic.eq_of_eq_coe (quadraticChar_isQuadratic F) isQuadratic_χ₈ hF
    ((quadraticChar_eq_pow_of_char_ne_two' hF 2).trans (FiniteField.two_pow_card hF))

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