infty_isScalarTower — Mathlib

English

The space lp B ∞ supports a scalar tower: 𝕜 acting on (lp B ∞) via 𝕜' acting on 𝕜 and then on the components B i.

Русский

Пространство lp B ∞ поддерживает торовоoе действие скаляров: 𝕜 действует на lp B ∞ через 𝕜' и затем через компоненты B_i.

LaTeX

$$$IsScalarTower 𝕜 (lp B ∞) (lp B ∞)$$$

Lean4

instance infty_isScalarTower {𝕜} [NormedRing 𝕜] [∀ i, Module 𝕜 (B i)] [∀ i, IsBoundedSMul 𝕜 (B i)]
    [∀ i, IsScalarTower 𝕜 (B i) (B i)] : IsScalarTower 𝕜 (lp B ∞) (lp B ∞) :=
  ⟨fun r f g => lp.ext <| smul_assoc (N := ∀ i, B i) (α := ∀ i, B i) r (⇑f) (⇑g)⟩

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