compProd_smul_left — Mathlib

English

Scaling μ by a scalar a scales the composition product by the same scalar: (a • μ) ⊗ₘ κ = a • (μ ⊗ₘ κ).

Русский

Умножение μ на скаляр a умножает композиционный продукт на такой же скаляр.

LaTeX

$$$(a \\cdot μ) ⊗ₘ κ = a \\cdot (μ ⊗ₘ κ)$$$

Lean4

theorem compProd_smul_left (a : ℝ≥0∞) [SFinite μ] [IsSFiniteKernel κ] : (a • μ) ⊗ₘ κ = a • (μ ⊗ₘ κ) :=
  by
  ext s hs
  simp only [compProd_apply hs, lintegral_smul_measure, smul_apply, smul_eq_mul]

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