instIsCentralScalar — Mathlib

English

The action of scalars on measures is central: for every scalar r, the left and right actions coincide in the sense described by the central scalar condition.

Русский

Действие скаляров на меры центрально: левое и правое действия совпадают в смысле условия центрального скаляра.

LaTeX

$$$\text{IsCentralScalar } R\,(\text{Measure}(\alpha)).$$$

Lean4

instance instIsCentralScalar [SMul Rᵐᵒᵖ ℝ≥0∞] [IsCentralScalar R ℝ≥0∞] {_ : MeasurableSpace α} :
    IsCentralScalar R (Measure α) :=
  ⟨fun _ _ => ext fun _ _ => op_smul_eq_smul _ _⟩

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