instIsCentralScalarPreLp — Mathlib

English

Let (E i) be normed additive groups with compatible module structures. Then the space PreLp E has a central scalar action by 𝕜; i.e., scalars from 𝕜 commute with all module operators on PreLp E.

Русский

Пусть (E_i) — нормированные аддитивные группы с совместимой структурой модуля; пространство PreLp E имеет центральное действие скаляров из 𝕜, то есть скаляры из 𝕜 commute с операторами модуля на PreLp E.

LaTeX

$$$IsCentralScalar 𝕜 (PreLp E)$$$

Lean4

instance [∀ i, Module 𝕜ᵐᵒᵖ (E i)] [∀ i, IsCentralScalar 𝕜 (E i)] : IsCentralScalar 𝕜 (PreLp E) :=
  Pi.isCentralScalar

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