instStarModuleSubtypePreLpMemAddSubgroup

Mathlib.Analysis.Normed.Lp.lpSpace

URI: https://scilib.ai/kg/mathlib#lp.instStarModuleSubtypePreLpMemAddSubgroup

English

There is a SmulCommClass between 𝕜 and the lp ∞-space: scalar multiplication commutes with space operations on lp ∞.

Русский

Существует SmulCommClass между 𝕜 и lp ∞: скалярное умножение коммутирует с операциями над lp ∞.

LaTeX

$$$SmulCommClass 𝕜 (lp B ∞) (lp B ∞)$$$

Lean4

instance : StarModule 𝕜 (lp E p) where star_smul _r _f := ext <| star_smul (A := ∀ i, E i) _ _

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

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

Разделы

Аффилиация

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