instIsCentralScalar — Mathlib

English

OuterMeasure α is a central scalar module over R; scalar actions commute with measure.

Русский

Область внешних мер α образует центральное скалярное пространство над R; скалярное действие коммутирует с мерой.

LaTeX

$$$\\text{IsCentralScalar } R (\\text{OuterMeasure } \\alpha)$$$

Lean4

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

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