minimalPeriod_of_comp_dvd_mul — Mathlib

English

If f and g commute, then the minimal period of f ∘ g divides the product of the minimal periods of f and g at x.

Русский

Если f и g commute, то минимальный период композиции f ∘ g в x делит произведение минимальных периодов f и g в x.

LaTeX

$$$ \\operatorname{minimalPeriod}(f \\circ g) x \\mid \\operatorname{minimalPeriod} f x \\cdot \\operatorname{minimalPeriod} g x $$$

Lean4

theorem minimalPeriod_of_comp_dvd_mul {g : α → α} (h : Commute f g) :
    minimalPeriod (f ∘ g) x ∣ minimalPeriod f x * minimalPeriod g x :=
  dvd_trans h.minimalPeriod_of_comp_dvd_lcm (lcm_dvd_mul _ _)

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