instSMul — Mathlib

English

There is a scalar action of R on FiniteMeasure Ω given by c • μ := ⟨c • (μ : Measure Ω), ...⟩, compatible with the tower conditions.

Русский

Существует скалярное действие R на FiniteMeasure Ω, задаваемое как c • μ = ⟨c • (μ : Measure Ω), ...⟩, совместимое с требуемыми условиями.

LaTeX

$$instance instSMul : SMul R (FiniteMeasure Ω) where smul (c : R) μ := ⟨c • (μ : Measure Ω), MeasureTheory.isFiniteMeasureSMulOfNNRealTower⟩$$

Lean4

instance instSMul : SMul R (FiniteMeasure Ω) where
  smul (c : R) μ := ⟨c • (μ : Measure Ω), MeasureTheory.isFiniteMeasureSMulOfNNRealTower⟩

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