mod_left

Mathlib.Tactic.NormNum.LegendreSymbol

URI: https://scilib.ai/kg/mathlib#Mathlib.Meta.NormNum.JacobiSym.mod_left

Lean4

/-- The value depends only on the residue class of `a` mod `b`. -/
theorem mod_left (a : ℤ) (b ab' : ℕ) (ab r b' : ℤ) (hb' : (b : ℤ) = b') (hab : a % b' = ab) (h : (ab' : ℤ) = ab)
    (hr : jacobiSymNat ab' b = r) : jacobiSym a b = r := by rw [← hr, jacobiSymNat, jacobiSym.mod_left, hb', hab, ← h]

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

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

Разделы

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

Аффилиация

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