minimalPeriod_eq_prime_iff — Mathlib

English

For a prime p, minimalPeriod f x = p iff IsPeriodicPt f p x and ¬IsFixedPt f x.

Русский

Для простого p: минимальный период f x равен p тогда и только тогда, когда x периодична с периодом p и не является фиксированной точкой.

LaTeX

$$$ \\mathrm{minimalPeriod} f x = p \\iff (\\mathrm{IsPeriodicPt} f p x) \\land \\neg (\\mathrm{IsFixedPt} f x) $$$

Lean4

theorem minimalPeriod_eq_prime_iff {p : ℕ} [hp : Fact p.Prime] :
    minimalPeriod f x = p ↔ IsPeriodicPt f p x ∧ ¬IsFixedPt f x :=
  by
  rw [Function.isPeriodicPt_iff_minimalPeriod_dvd, Nat.dvd_prime hp.out, ← minimalPeriod_eq_one_iff_isFixedPt.not,
    or_and_right, and_not_self_iff, false_or, iff_self_and]
  exact fun h ↦ ne_of_eq_of_ne h hp.out.ne_one

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