mod_left'

Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

URI: https://scilib.ai/kg/mathlib#jacobiSym.mod_left'

← MathLib Explorer

English

If a1 ≡ a2 (mod b), then J(a1 | b) = J(a2 | b).

Русский

Если a1 ≡ a2 (mod b), то J(a1 | b) = J(a2 | b).

LaTeX

$$$ a_1 \equiv a_2 \pmod{b} \Rightarrow J(a_1 | b) = J(a_2 | b) $$$

Lean4

/-- The symbol `J(a | b)` depends only on `a` mod `b`. -/
theorem mod_left' {a₁ a₂ : ℤ} {b : ℕ} (h : a₁ % b = a₂ % b) : J(a₁ | b) = J(a₂ | b) := by rw [mod_left, h, ← mod_left]

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

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

Разделы

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

Аффилиация

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