quadraticChar_odd_prime — Mathlib

English

For odd prime p with p ≠ ringChar F, the value χF(p) is related to the quadratic character modulo p via comparison with χFp and χp.

Русский

Для нечеткого простого p с p ≠ ringChar F значение χF(p) связано через χp и χFp.

LaTeX

$$$χ_F(p) = χ_p( χ_4(|F|) \cdot |F| )$$$

Lean4

/-- The value of the quadratic character at an odd prime `p` different from `ringChar F`. -/
theorem quadraticChar_odd_prime [DecidableEq F] (hF : ringChar F ≠ 2) {p : ℕ} [Fact p.Prime] (hp₁ : p ≠ 2)
    (hp₂ : ringChar F ≠ p) : quadraticChar F p = quadraticChar (ZMod p) (χ₄ (Fintype.card F) * Fintype.card F) :=
  by
  rw [← quadraticChar_neg_one hF]
  have h :=
    quadraticChar_card_card hF (ne_of_eq_of_ne (ringChar_zmod_n p) hp₁) (ne_of_eq_of_ne (ringChar_zmod_n p) hp₂.symm)
  rwa [card p] at h

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