quadraticChar_neg_two — Mathlib

English

The value of the quadratic character at −2 is given by a product of χ₈' and χ₄ evaluated at the field size, transported to F.

Русский

Значение χF(−2) задаётся через χ₈' и χ₄, применяемые к размеру поля и перенесённые в F.

LaTeX

$$$χ_F(-2) = χ_8'( |F| ) (\text{cast}) · χ_4(|F|)^{?}$$$

Lean4

/-- The value of the quadratic character at `-2` -/
theorem quadraticChar_neg_two [DecidableEq F] (hF : ringChar F ≠ 2) : quadraticChar F (-2) = χ₈' (Fintype.card F) := by
  rw [(by simp : (-2 : F) = -1 * 2), map_mul, χ₈'_eq_χ₄_mul_χ₈, quadraticChar_neg_one hF, quadraticChar_two hF,
    @cast_natCast _ (ZMod 4) _ _ _ (by decide : 4 ∣ 8)]

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