coe_pow

Mathlib.Topology.Algebra.Module.LinearMap

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

English

For endomorphisms f, g and x, (f * g) x = f (g x).

Русский

Для эндоморфизмов f, g и элемента x выполняется (f * g) x = f(g(x)).

LaTeX

$$$ (f * g) x = f (g x) $$$

Lean4

theorem coe_pow (f : M₁ →L[R₁] M₁) (n : ℕ) : ⇑(f ^ n) = f^[n] :=
  hom_coe_pow _ rfl (fun _ _ ↦ rfl) _ _

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

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

Разделы

Аффилиация

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