coe_pow — Mathlib

English

Let f be a star-algebra automorphism of R over S. Then the underlying function of f^n equals the n-fold iterate of the underlying function of f.

Русский

Пусть f — автоморфизм звездной алгебры R над S. Тогда функция, лежащая в основе f^n, равна n-кратному применению функции f.

LaTeX

$$$ \forall x,\ (f^n)(x) = f^{\circ n}(x). $$$

Lean4

@[simp]
theorem coe_pow (f : R ≃⋆ₐ[S] R) (n : ℕ) : ⇑(f ^ n) = (⇑f)^[n] :=
  hom_coe_pow _ (funext one_apply) (fun f g ↦ funext <| mul_apply f g) _ _

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