pow_period_add_smul

Mathlib.Dynamics.PeriodicPts.Defs

URI: https://scilib.ai/kg/mathlib#MulAction.pow_period_add_smul

← MathLib Explorer

English

For i ∈ Z, g^(i + period g a) • a = g^i • a.

Русский

Для i ∈ Z выполняется: g^(i + period g a) • a = g^i • a.

LaTeX

$$$ g^{(i + \\operatorname{period}(g,a))} \\cdot a = g^{i} \\cdot a $$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru