to_jacobiSym

Mathlib.Tactic.NormNum.LegendreSymbol

URI: https://scilib.ai/kg/mathlib#Mathlib.Meta.NormNum.LegendreSym.to_jacobiSym

Lean4

/-- Turn a Legendre symbol into a Jacobi symbol. -/
theorem to_jacobiSym (p : ℕ) (pp : Fact p.Prime) (a r : ℤ) (hr : IsInt (jacobiSym a p) r) : IsInt (legendreSym p a) r :=
  by rwa [@jacobiSym.legendreSym.to_jacobiSym p pp a]

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

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

Разделы

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

Аффилиация

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