smul_compLpL — Mathlib

English

Scalar multiplication commutes with the Lp-composition, i.e., (c • L) ∘ f = c • (L ∘ f).

Русский

Умножение на скаляр и композиция в Lp коммутируют: (c•L) ∘ f = c•(L ∘ f).

LaTeX

$$$ (c \\cdot L)\\circ f = c \\cdot (L\\circ f).$$$

Lean4

theorem smul_compLpL [Fact (1 ≤ p)] {𝕜''} [NormedRing 𝕜''] [Module 𝕜'' F] [IsBoundedSMul 𝕜'' F] [SMulCommClass 𝕜' 𝕜'' F]
    (c : 𝕜'') (L : E →SL[σ] F) : (c • L).compLpL p μ = c • L.compLpL p μ := by ext1 f; exact smul_compLp c L f

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