English
Let f and g be commuting maps on a set α. If the minimal periods of f at x and of g at x are coprime, then the minimal period of the composition f ∘ g at x equals the product of the two minimal periods: minimalPeriod(f ∘ g, x) = minimalPeriod(f, x) · minimalPeriod(g, x).
Русский
Пусть f и g — перестановочные отображения на множестве, удовлетворяющем f ∘ g, и пусть x ∈ α. Если минимальные периоды f при x и g при x взаимно просты, то минимальный период композиции f ∘ g при x равен произведению минимальных периодов: minimalPeriod(f ∘ g, x) = minimalPeriod(f, x) · minimalPeriod(g, x).
LaTeX
$$$\text{minimalPeriod}(f \circ g, x) = \text{minimalPeriod}(f, x) \cdot \text{minimalPeriod}(g, x)$,\quad \text{provided } \gcd(\text{minimalPeriod}(f, x), \text{minimalPeriod}(g, x)) = 1.$$$
Lean4
theorem minimalPeriod_of_comp_eq_mul_of_coprime {g : α → α} (h : Commute f g)
(hco : Coprime (minimalPeriod f x) (minimalPeriod g x)) :
minimalPeriod (f ∘ g) x = minimalPeriod f x * minimalPeriod g x :=
by
apply h.minimalPeriod_of_comp_dvd_mul.antisymm
suffices
∀ {f g : α → α},
Commute f g → Coprime (minimalPeriod f x) (minimalPeriod g x) → minimalPeriod f x ∣ minimalPeriod (f ∘ g) x
from hco.mul_dvd_of_dvd_of_dvd (this h hco) (h.comp_eq.symm ▸ this h.symm hco.symm)
intro f g h hco
refine hco.dvd_of_dvd_mul_left (IsPeriodicPt.left_of_comp h ?_ ?_).minimalPeriod_dvd
· exact (isPeriodicPt_minimalPeriod _ _).const_mul _
· exact (isPeriodicPt_minimalPeriod _ _).mul_const _
