instModule

Mathlib.MeasureTheory.Function.LpSpace.Basic

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Lp.instModule

English

Equality of module structures induced on Lp spaces.

Русский

Равенство структур модуля на пространствах Lp.

LaTeX

$$$Lp\; \text{module} \; = \; Lp\; \text{module}$$$

Lean4

instance instModule : Module 𝕜 (Lp E p μ) :=
  { (LpSubmodule 𝕜 E p μ).module with }

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

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

Разделы

Аффилиация

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