minimalPeriod_iterate_eq_div_gcd — Mathlib

English

For n ≠ 0, the minimal period of the nth iterate of f is equal to the minimal period divided by gcd(minimalPeriod(f,x), n) provided x is a periodic point of f.

Русский

Для n ≠ 0 минимальный период итерации f^{[n]} в точке x равен минимальному периоду f x делённому на gcd(minimalPeriod(f,x), n), если x периодична по f.

LaTeX

$$$\\operatorname{minimalPeriod}(f^{[n]},x) = \\operatorname{minimalPeriod}(f,x) / \\gcd(\\operatorname{minimalPeriod}(f,x), n)$$$

Lean4

theorem minimalPeriod_iterate_eq_div_gcd (h : n ≠ 0) :
    minimalPeriod f^[n] x = minimalPeriod f x / Nat.gcd (minimalPeriod f x) n :=
  minimalPeriod_iterate_eq_div_gcd_aux <| gcd_pos_of_pos_right _ (Nat.pos_of_ne_zero h)

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