iterate_map_pow — Mathlib

English

Iterating preserves natural 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},\\; k\\in\\mathbb{N}.$$$

Lean4

@[to_additive (attr := simp)]
theorem iterate_map_pow {M F : Type*} [Monoid 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_pow f · k) n x

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