at_neg_one — Mathlib

English

Let p be a prime with p ≠ 2. Then the Legendre symbol (−1/p) equals χ4(p), where χ4 is the quadratic character modulo 4.

Русский

Пусть p — простое число, p ≠ 2. Тогда знак Лежандра (−1/p) равен χ4(p), где χ4 — квадратичный символ модуля 4.

LaTeX

$$$\\left( \\frac{-1}{p} \\right) = \\chi_4(p)$$$

Lean4

/-- `legendreSym p (-1)` is given by `χ₄ p`. -/
theorem at_neg_one (hp : p ≠ 2) : legendreSym p (-1) = χ₄ p := by
  simp only [legendreSym, card p, quadraticChar_neg_one ((ringChar_zmod_n p).substr hp), Int.cast_neg, Int.cast_one]

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