applySMulCommClass'

Mathlib.Topology.Algebra.Module.LinearMap

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.applySMulCommClass'

English

Applying the codRestrict map to x yields the same as applying f to x and then restricting.

Русский

Применение codRestrict к x равно приложению f к x с ограничением.

LaTeX

$$$ (f.codRestrict p h) x = f x $$$

Lean4

instance applySMulCommClass' : SMulCommClass (M₁ →L[R₁] M₁) R₁ M₁ where smul_comm := ContinuousLinearMap.map_smul

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

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

Разделы

Аффилиация

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