comp_lcm — Mathlib

English

If f and g commute and x is periodic with periods m and n, then f ∘ g has period lcm(m,n) at x.

Русский

Если f и g коммутируют и x периодичен с периодами m и n, то f ∘ g имеет период \\mathrm{lcm}(m,n) в точке x.

LaTeX

$$%%$$

Lean4

theorem comp_lcm {g : α → α} (hco : Commute f g) (hf : IsPeriodicPt f m x) (hg : IsPeriodicPt g n x) :
    IsPeriodicPt (f ∘ g) (Nat.lcm m n) x :=
  (hf.trans_dvd <| Nat.dvd_lcm_left _ _).comp hco (hg.trans_dvd <| Nat.dvd_lcm_right _ _)

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