coe_pow

Mathlib.Algebra.Ring.Hom.Defs

URI: https://scilib.ai/kg/mathlib#RingHom.coe_pow

English

The underlying function of f^n equals the n-fold iterate of the underlying function of f.

Русский

Функциональное отображение f^n равно n-кратной итерации базовой функции f.

LaTeX

$$$\big( f^n \big)\!:\alpha \to \alpha = f^{\circ n}$$$

Lean4

@[simp, norm_cast]
theorem coe_pow (f : α →+* α) (n : ℕ) : ⇑(f ^ n) = f^[n] :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru