quadraticChar_neg_one — Mathlib

English

The quadratic character evaluated at −1 has a closed form in terms of χ₄ (the mod 4 character) and card F.

Русский

Значение χF(−1) задаётся через χ₄ и размер поля.

LaTeX

$$$χ_F(-1) = χ_4(|F|)\;\text{(cast to appropriate codomain)}$$$

Lean4

/-- The value of the quadratic character at `-1` -/
theorem quadraticChar_neg_one [DecidableEq F] (hF : ringChar F ≠ 2) : quadraticChar F (-1) = χ₄ (Fintype.card F) :=
  by
  have h := quadraticChar_eq_pow_of_char_ne_two hF (neg_ne_zero.mpr one_ne_zero)
  rw [h, χ₄_eq_neg_one_pow (FiniteField.odd_card_of_char_ne_two hF)]
  generalize Fintype.card F / 2 = n
  rcases Nat.even_or_odd n with h₂ | h₂
  · simp only [Even.neg_one_pow h₂, if_true]
  · simp only [Odd.neg_one_pow h₂, Ring.neg_one_ne_one_of_char_ne_two hF, ite_false]

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