zpow_smul_eq_iff_minimalPeriod_dvd

English

For integer j, a^j fixes b iff the cast of minimalPeriod (a•) b to ℤ divides j.

Русский

Для целого j: a^j фиксирует b тогда, когда отображение минимального периода приводится к делению j по модулю ℤ.

LaTeX

$$$ \\mathrm{IsFixedPt}\\ (a^j, b) \\iff (\\operatorname{minimalPeriod}(a \\cdot ) b : \\mathbb{Z}) \\mid j $$$

Lean4

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

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