at_two

Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

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

← MathLib Explorer

English

If b is odd, J(2 | b) = χ₈(b).

Русский

Если b нечётно, J(2 | b) = χ₈(b).

LaTeX

$$$ J(2 | b) = χ_8(b) $$$

Lean4

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

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

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

Разделы

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

Аффилиация

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