toIocMod_periodic

Mathlib.Algebra.Order.ToIntervalMod

URI: https://scilib.ai/kg/mathlib#toIocMod_periodic

English

Function toIocMod hp a is periodic with period p: Function.Periodic (toIocMod hp a) p.

Русский

Функция toIocMod hp a периодична с периодом p: Function.Periodic (toIocMod hp a) p.

LaTeX

$$$ \\text{Function.Periodic}\\ (toIocMod\\ hp\\ a)\\ p $$$

Lean4

theorem toIocMod_periodic (a : α) : Function.Periodic (toIocMod hp a) p :=
  toIocMod_add_right hp a

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

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

Разделы

Аффилиация

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