at_neg_two

Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity

URI: https://scilib.ai/kg/mathlib#legendreSym.at_neg_two

← MathLib Explorer

English

For p ≠ 2, the Legendre symbol (−2/p) equals χ8'(p).

Русский

для p ≠ 2, (−2/p) = χ8'(p).

LaTeX

$$$\left(\frac{-2}{p}\right) = χ_8'(p)$$$

Lean4

/-- `legendreSym p (-2)` is given by `χ₈' p`. -/
theorem at_neg_two (hp : p ≠ 2) : legendreSym p (-2) = χ₈' p :=
  by
  have : (-2 : ZMod p) = (-2 : ℤ) := by norm_cast
  rw [legendreSym, ← this, quadraticChar_neg_two ((ringChar_zmod_n p).substr hp), card p]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru