at_two

Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity

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

← MathLib Explorer

English

For a prime 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_two (hp : p ≠ 2) : legendreSym p 2 = χ₈ p :=
  by
  have : (2 : ZMod p) = (2 : ℤ) := by norm_cast
  rw [legendreSym, ← this, quadraticChar_two ((ringChar_zmod_n p).substr hp), card p]

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

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

Разделы

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

Аффилиация

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