minimalPeriod_dvd — Mathlib

English

If x is periodic with period n under f, then the minimal period of x divides n.

Русский

Если x периодично повторяется с периодом n относительно f, то минимальный период x делится на n.

LaTeX

$$$\\operatorname{IsPeriodicPt}(f,n,x) \\Rightarrow \\operatorname{minimalPeriod}(f,x) \\mid n$$$

Lean4

theorem minimalPeriod_dvd (hx : IsPeriodicPt f n x) : minimalPeriod f x ∣ n :=
  (eq_or_lt_of_le <| n.zero_le).elim (fun hn0 => hn0 ▸ Nat.dvd_zero _) fun hn0 =>
    Nat.dvd_iff_mod_eq_zero.2 <|
      (hx.mod <| isPeriodicPt_minimalPeriod f x).eq_zero_of_lt_minimalPeriod <| Nat.mod_lt _ <| hx.minimalPeriod_pos hn0

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