coe_pow — Mathlib

English

For a C^n-map f, the underlying function satisfies that the i-th iterate power has the same underlying function as taking power pointwise: the differentiation structure is preserved under taking powers.

Русский

Кнопка f^n имеет такое же подлежащие отображение, как и точечное возведение в степень; структура гладкости сохраняется при возведении в степень.

LaTeX

$$$\widehat{f^n} = \widehat{f}^n\quad\text{where } \widehat{f} = f\text{ as a function }N\to G.$$$

Lean4

@[to_additive (attr := simp)]
theorem coe_pow {G : Type*} [Monoid G] [TopologicalSpace G] [ChartedSpace H' G] [ContMDiffMul I' n G]
    (f : C^n⟮I, N; I', G⟯) (n : ℕ) : ⇑(f ^ n) = (f : N → G) ^ n :=
  rfl

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