instNatCast

Mathlib.Topology.Algebra.Module.LinearMap

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.instNatCast

English

The nth power f^n of a continuous linear endomorphism corresponds to the nth iterate f^[n] of the underlying function.

Русский

Степень n эндоморфизма f^n соответствует n-й итерации функции f^[n].

LaTeX

$$$ (f^n) = f^{[n]} $$$

Lean4

instance instNatCast [ContinuousAdd M₁] : NatCast (M₁ →L[R₁] M₁) where natCast n := n • (1 : M₁ →L[R₁] M₁)

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

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

Разделы

Аффилиация

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