χ₈_int_mod_eight

Mathlib.NumberTheory.LegendreSymbol.ZModChar

URI: https://scilib.ai/kg/mathlib#ZMod.χ₈_int_mod_eight

← MathLib Explorer

English

χ₈(n) = χ₈(n mod 8) for integers n.

Русский

χ₈(n) = χ₈(n mod 8) для целых n.

LaTeX

$$$ χ_{8}(n) = χ_{8}(n \\bmod 8) $ for all n ∈ \\mathbb{Z}. $$

Lean4

/-- The value of `χ₈ n`, for `n : ℤ`, depends only on `n % 8`. -/
theorem χ₈_int_mod_eight (n : ℤ) : χ₈ n = χ₈ (n % 8 : ℤ) := by rw [← ZMod.intCast_mod n 8, Nat.cast_ofNat]

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

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

Разделы

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

Аффилиация

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