periodic_mod

Mathlib.Data.Nat.Periodic

URI: https://scilib.ai/kg/mathlib#Nat.periodic_mod

English

For any a, the function n ↦ n mod a is periodic with period a; i.e., n mod a = (n+a) mod a for all n.

Русский

Для любого a функция n mod a периодична с периодом a; то есть n mod a = (n+a) mod a для всех n.

LaTeX

$$$ \forall n, n \bmod a = (n+a) \bmod a $$$

Lean4

theorem periodic_mod (a : ℕ) : Periodic (fun n => n % a) a := by simp only [forall_const, add_mod_right, Periodic]

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

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

Разделы

Аффилиация

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