χ₄_int_mod_four

Mathlib.NumberTheory.LegendreSymbol.ZModChar

URI: https://scilib.ai/kg/mathlib#ZMod.χ₄_int_mod_four

← MathLib Explorer

English

The value of χ₄ on integers depends only on n mod 4.

Русский

Значение χ₄ на целых числах зависит только от n mod 4.

LaTeX

$$$ χ_{4}(n) \\text{ depends only on } n \\bmod 4. $$$

Lean4

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

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

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

Разделы

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

Аффилиация

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