coe_pow — Mathlib

English

The underlying function corresponding to the nth power equals the nth iterate: for f ∈ AddConstMap G G a a, and n ∈ ℕ, coe(f^n) = f^[n].

Русский

Функция-основание, соответствующая n-й степени, равна n-й итерации: для f ∈ AddConstMap G G a a и n ∈ ℕ выполняется coe(f^n) = f^[n].

LaTeX

$$$\operatorname{coe}(f^n) = f^{[n]} \quad (n \in \mathbb{N})$$$

Lean4

@[simp, push_cast]
theorem coe_pow (f : G →+c[a, a] G) (n : ℕ) : ⇑(f ^ n) = f^[n] :=
  rfl

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