minimalPeriod_iterate_eq_div_gcd'

English

If x is a periodic point of f, then the same gcd-based formula for minimal period holds for the nth iterate of f.

Русский

Если x — периодическая точка относительно f, то та же формула на основе НОД применяется к минимальному периоду итерата f по n.

LaTeX

$$$\\text{(h)}\\ x \\in \\operatorname{periodicPts}(f)\\Rightarrow \\operatorname{minimalPeriod}(f^{[n]},x) = \\operatorname{minimalPeriod}(f,x) / \\gcd(\\operatorname{minimalPeriod}(f,x), n)$$$

Lean4

theorem minimalPeriod_iterate_eq_div_gcd' (h : x ∈ periodicPts f) :
    minimalPeriod f^[n] x = minimalPeriod f x / Nat.gcd (minimalPeriod f x) n :=
  minimalPeriod_iterate_eq_div_gcd_aux <| gcd_pos_of_pos_left n (minimalPeriod_pos_iff_mem_periodicPts.mpr h)

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