isMulLeftInvariant_smul — Mathlib

English

If μ is right-invariant, then c • μ is right-invariant for any c ∈ ENNReal.

Русский

Если μ инвариантна справа, то c • μ инвариантна справа для любого c ∈ ENNReal.

LaTeX

$$$[IsMulRightInvariant\\, \\mu] \\Rightarrow [IsMulRightInvariant\\, (c \\cdot \\mu)]$$$

Lean4

@[to_additive MeasureTheory.isAddLeftInvariant_smul]
instance isMulLeftInvariant_smul [IsMulLeftInvariant μ] (c : ℝ≥0∞) : IsMulLeftInvariant (c • μ) :=
  ⟨fun g => by rw [Measure.map_smul, map_mul_left_eq_self]⟩

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