English
If f and g commute (i.e., f∘g = g∘f), then the minimal period of the composition at x divides the least common multiple of the minimal periods of f and g at x.
Русский
Если f и g коммутируют (то есть f∘g = g∘f), то минимальный период композиции f∘g в точке x делит НОК минимальних периодов f в x и g в x.
LaTeX
$$$\\operatorname{minimalPeriod}(f\\circ g,x) \\mid \\operatorname{lcm}(\\operatorname{minimalPeriod}(f,x), \\operatorname{minimalPeriod}(g,x))$$$
Lean4
theorem minimalPeriod_of_comp_dvd_lcm {g : α → α} (h : Commute f g) :
minimalPeriod (f ∘ g) x ∣ Nat.lcm (minimalPeriod f x) (minimalPeriod g x) :=
by
rw [← isPeriodicPt_iff_minimalPeriod_dvd]
exact (isPeriodicPt_minimalPeriod f x).comp_lcm h (isPeriodicPt_minimalPeriod g x)