pow_smul_eq_iff_minimalPeriod_dvd

English

For a, f, and x, the statement a^n • b = b is equivalent to minimalPeriod f x dividing n; in particular, there is a link between fixed and periodic behavior.

Русский

Для a, f и x утверждение a^n • b = b эквивалентно тому, что минимальный период делит n; существует связь между фиксированным и периодическим поведением.

LaTeX

$$$ \\text{MinimalPeriod} \\ (f, x) \\mid n \\Leftrightarrow \\cdots $$$

Lean4

@[to_additive]
theorem pow_smul_eq_iff_minimalPeriod_dvd {n : ℕ} : a ^ n • b = b ↔ minimalPeriod (a • ·) b ∣ n := by
  rw [← period_eq_minimalPeriod, pow_smul_eq_iff_period_dvd]

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