pow_add_period_smul — Mathlib

English

For natural n and action m on a, m^(period m a + n) • a = m^n • a.

Русский

Для натурального n и действия m на a выполняется: m^(period m a + n) • a = m^n • a.

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem pow_add_period_smul (n : ℕ) (m : M) (a : α) : m ^ (n + period m a) • a = m ^ n • a := by
  rw [← pow_mod_period_smul, Nat.add_mod_right, pow_mod_period_smul]

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