pow_mod_period_smul — Mathlib

English

For prime p, minimalPeriod f x = p if and only if f x is p-periodic and x is not fixed; equivalently, IsPeriodicPt f p x and not IsFixedPt f x.

Русский

Для простого p минимальный период функции f в точке x равен p тогда и только тогда, когда x периодична с периодом p и не является фиксированной точкой.

LaTeX

$$$ \\mathrm{minimalPeriod}\\ f\\ x = p \\iff (\\mathrm{IsPeriodicPt}\\ f\\ p\\ x) \\land \\neg (\\mathrm{IsFixedPt}\\ f\\ x) $$$

Lean4

@[to_additive (attr := simp)]
theorem pow_mod_period_smul (n : ℕ) {m : M} {a : α} : m ^ (n % period m a) • a = m ^ n • a := by
  conv_rhs =>
    rw [← Nat.mod_add_div n (period m a), pow_add, mul_smul, pow_smul_eq_iff_period_dvd.mpr (dvd_mul_right _ _)]

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