minimalPeriod_eq_minimalPeriod_iff

English

If n ≠ 0, then the minimal period of the nth iterate f^[n] at x is equal to minimalPeriod(f,x) divided by gcd(minimalPeriod(f,x), n).

Русский

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

LaTeX

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

Lean4

theorem minimalPeriod_eq_minimalPeriod_iff {g : β → β} {y : β} :
    minimalPeriod f x = minimalPeriod g y ↔ ∀ n, IsPeriodicPt f n x ↔ IsPeriodicPt g n y := by
  simp_rw [isPeriodicPt_iff_minimalPeriod_dvd, dvd_right_iff_eq]

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