smul_comm — Mathlib

English

The smul by a scalar commutes with the Lp-multiplication: c • f • g = f • c • g.

Русский

Скалярное умножение commuting с произведением в Lp: c • f • g = f • c • g.

LaTeX

$$$$ \forall c \in \mathbb{K}', \ f \in L^p(\mu), \ g \in L^q(\mu): c \cdot f \cdot g = f \cdot c \cdot g. $$$$

Lean4

protected theorem smul_comm [SMulCommClass 𝕜' 𝕜 E] (c : 𝕜') (f : Lp 𝕜 p μ) (g : Lp E q μ) : c • f • g = f • c • g :=
  by
  simp only [smul_def, ← MemLp.toLp_const_smul]
  apply MemLp.toLp_congr
  filter_upwards [Lp.coeFn_smul c f, Lp.coeFn_smul c g] with x hfx hgx
  simp [smul_comm, hgx]

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