instPowNat — Mathlib

English

There is a natural-power structure on the endomorphisms G →+c[a,a] G, i.e., powers correspond to iterates of the underlying map.

Русский

Существует естественная операция возведения в степень на концевых отображениях G →+c[a,a] G, то есть степени соответствуют повторным применениям отображения.

LaTeX

$$$\text{Pow} (G \to+c[a,a] G) \, \mathbb{N} \;\text{is defined by } f^n = \text{iterate}(f, n).$$$

Lean4

instance : Pow (G →+c[a, a] G) ℕ where pow f n := ⟨f^[n], Commute.iterate_left (AddConstMapClass.semiconj f) _⟩

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