mod

Mathlib.Dynamics.PeriodicPts.Defs

URI: https://scilib.ai/kg/mathlib#Function.IsPeriodicPt.mod

English

If x is periodic with periods m and n for f, then x is periodic with period m mod n.

Русский

Если x периодичен с периодами m и n для f, то x периодичен с периодом m mod n.

LaTeX

$$$IsPeriodicPt f m x \to IsPeriodicPt f n x \to IsPeriodicPt f (m \% n) x$$$

Lean4

protected theorem mod (hm : IsPeriodicPt f m x) (hn : IsPeriodicPt f n x) : IsPeriodicPt f (m % n) x :=
  (hn.iterate_mod_apply m).trans hm

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

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

Разделы

Аффилиация

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