pow_smul_eq_iff_period_dvd — Mathlib

English

For a MulAction setup, m^n • a = a holds if and only if period m a divides n.

Русский

Для мультидействия выполняется: m^n • a = a тогда и только тогда, когда период m a делится на n.

LaTeX

$$$ m^n \\cdot a = a \\iff \\operatorname{period}(m,a) \\mid n $$$

Lean4

@[to_additive]
theorem pow_smul_eq_iff_period_dvd {n : ℕ} {m : M} {a : α} : m ^ n • a = a ↔ period m a ∣ n := by
  rw [period_eq_minimalPeriod, ← isPeriodicPt_iff_minimalPeriod_dvd, isPeriodicPt_smul_iff]

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