English
In the framework of Lp-spaces, scalar multiplication associates with the Lp-product: for every scalar c in the scalar field, and for f in Lp and g in Lq, (c · f) · g = c · (f · g).
Русский
В пространствахLp ассоциативность скалярного умножения с произведением в Lp: для любого скаляра c из поля скаляров и для f в Lp и g в Lq выполняется (c · f) · g = c · (f · g).
LaTeX
$$$$ \forall c \in \mathbb{K}', \ f \in L^p(\mu), \ g \in L^q(\mu): (c \cdot f) \cdot g = c \cdot (f \cdot g). $$$$
Lean4
protected theorem smul_assoc [IsScalarTower 𝕜' 𝕜 E] (c : 𝕜') (f : Lp 𝕜 p μ) (g : Lp E q μ) :
(c • f) • g = c • (f • g) := by
simp only [smul_def, ← MemLp.toLp_const_smul]
apply MemLp.toLp_congr
filter_upwards [Lp.coeFn_smul c f] with x hx
simp [-smul_eq_mul, hx]
