zpow_add_period_smul — Mathlib

English

For any integer j, a^j • b = a^n • b is governed by the minimal period of a acting on b modulo j.

Русский

Для любого целого j применимость a^j к b определяется минимальным периодом действия a на b по модулю j.

LaTeX

$$$ a^{j} \\cdot b = b \\iff (\\operatorname{minimalPeriod}(a \\cdot \\!\\cdot) b : \\mathbb{Z}) \\mid j $$$

Lean4

@[to_additive (attr := simp)]
theorem zpow_add_period_smul (i : ℤ) (g : G) (a : α) : g ^ (i + period g a) • a = g ^ i • a := by
  rw [← zpow_mod_period_smul, Int.add_emod_right, zpow_mod_period_smul]

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