minimalPeriod_of_comp_dvd_lcm — Mathlib

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)

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