iterate_map_zpow — Mathlib

English

Iterating preserves integer powers: f^[n](x^k) = f^[n](x)^k for k ∈ ℤ.

Русский

Итерация сохраняет целочисленные степени: f^[n](x^k) = f^[n](x)^k для k ∈ ℤ.

LaTeX

$$$f^{[n]}(x^{k}) = f^{[n]}(x)^{k}$ for all k ∈ ℤ.$$

Lean4

@[to_additive (attr := simp)]
theorem iterate_map_zpow {M F : Type*} [Group M] [FunLike F M M] [MonoidHomClass F M M] (f : F) (n : ℕ) (x : M)
    (k : ℤ) : f^[n] (x ^ k) = f^[n] x ^ k :=
  Commute.iterate_left (map_zpow f · k) n x

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