English
Let (E i) be a family of normed additive groups indexed by α, and let 𝕜, 𝕜' be normed rings equipped with a compatible scalar action and a scalar-tower structure on each E i. Then the pointwise space PreLp E carries a natural IsScalarTower structure: 𝕜' → 𝕜 → PreLp E.
Русский
Пусть (E_i) — семейство нормированных аддитивных групп, индексируемых по α; кольца 𝕜 и 𝕜' — нормированные, имеющие совместное скалярное действие, и на каждом E_i задана совместимая структура торов. Тогда пространство PreLp E естественным образом наследует структуру IsScalarTower: 𝕜' → 𝕜 → PreLp E.
LaTeX
$$$IsScalarTower 𝕜' 𝕜 (PreLp E)$$$
Lean4
instance [SMul 𝕜' 𝕜] [∀ i, IsScalarTower 𝕜' 𝕜 (E i)] : IsScalarTower 𝕜' 𝕜 (PreLp E) :=
Pi.isScalarTower
