iterate_succ

Mathlib.Algebra.Module.LinearMap.End

URI: https://scilib.ai/kg/mathlib#Module.End.iterate_succ

English

The successor of the iterate satisfies f'^(n+1) = f'^n ∘ f'.

Русский

Следовательность итераций удовлетворяет f'^{n+1} = f'^n ∘ f'.

LaTeX

$$$f'^{n+1} = f'^n \\circ f'.$$$

Lean4

theorem iterate_succ (n : ℕ) : f' ^ (n + 1) = .comp (f' ^ n) f' := by rw [pow_succ, mul_eq_comp]

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

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

Разделы

Аффилиация

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