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)