English
Let e be a dilation self-equivalence of a space X. Then the nth power of e, viewed as a function, coincides with the nth iterate of the underlying function of e; that is, for every n, the function e^n equals the n-fold composition e∘…∘e (n times).
Русский
Пусть e — дилатационная эквивалентность пространства X в самом себе. Тогда для каждого натурального n функция e^n совпадает с n-кратной композицией функции, лежащей в основе e; то есть e^n = e^[n].
LaTeX
$$$ (e^n) = e^{[n]} $$$
Lean4
@[norm_cast]
theorem coe_pow (e : X ≃ᵈ X) (n : ℕ) : ⇑(e ^ n) = e^[n] := by
rw [← coe_toEquiv, ← toPerm_apply, map_pow, Equiv.Perm.coe_pow];
rfl
-- TODO: Once `IsometryEquiv` follows the `*EquivClass` pattern, replace this with an instance
-- of `DilationEquivClass` assuming `IsometryEquivClass`.
