zpow_smul_mod_minimalPeriod — Mathlib

English

For integer j, a^n • b = a^n' • b with mod applied via minimal period.

Русский

Для целого j: модуль минимального периода применяется к степени zpow.

LaTeX

$$$ a^{\\,n} \\cdot b = a^{\\,n'} \\cdot b \\text{ mod minimalPeriod } \\ (a\\cdot) b $$$

Lean4

@[to_additive (attr := simp)]
theorem zpow_smul_mod_minimalPeriod (n : ℤ) : a ^ (n % (minimalPeriod (a • ·) b : ℤ)) • b = a ^ n • b := by
  rw [← period_eq_minimalPeriod, zpow_mod_period_smul]

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