minimalPeriod_eq_prime_pow — Mathlib

English

If not IsPeriodicPt f (p^k) x but IsPeriodicPt f (p^(k+1)) x, then minimalPeriod f x = p^(k+1).

Русский

Если x не периодичен с периодом p^k, но периодичен с периодом p^(k+1), то минимальный период равен p^(k+1).

LaTeX

$$$ \\neg \\mathrm{IsPeriodicPt}\\ f\\ (p^k)\\ x \\land \\mathrm{IsPeriodicPt}\\ f\\ (p^{k+1})\\ x \\Rightarrow \\mathrm{minimalPeriod} f x = p^{k+1} $$$

Lean4

theorem minimalPeriod_eq_prime_pow {p k : ℕ} [hp : Fact p.Prime] (hk : ¬IsPeriodicPt f (p ^ k) x)
    (hk1 : IsPeriodicPt f (p ^ (k + 1)) x) : minimalPeriod f x = p ^ (k + 1) := by
  apply Nat.eq_prime_pow_of_dvd_least_prime_pow hp.out <;> rwa [← isPeriodicPt_iff_minimalPeriod_dvd]

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