pow_period_smul — Mathlib

English

In a MulAction setting, m^(period m a) • a = a; i.e., after the period acts, a is fixed by m^period on a.

Русский

В условиях MulAction после применения m^period(m,a) к a получаем a: m^(period m a) • a = a.

LaTeX

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

Lean4

/-- `m ^ (period m a)` fixes `a`. -/
@[to_additive (attr := simp) /-- `(period m a) • m` fixes `a`. -/
    ]
theorem pow_period_smul (m : M) (a : α) : m ^ (period m a) • a = a := by
  rw [period_eq_minimalPeriod, ← smul_iterate_apply, iterate_minimalPeriod]

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