at_neg_two

Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

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

← MathLib Explorer

English

For any a, J(a|0) equals 1.

Русский

Для любого a символ Якоби J(a|0) равен единице.

LaTeX

$$$J(a|0) = 1$$$

Lean4

/-- If `b` is odd, then `J(-2 | b)` is given by `χ₈' b`. -/
theorem at_neg_two {b : ℕ} (hb : Odd b) : J(-2 | b) = χ₈' b :=
  value_at (-2) χ₈'.toMonoidHom (fun p pp => @legendreSym.at_neg_two p ⟨pp⟩) hb

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

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

Разделы

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

Аффилиация

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