haarScalarFactor_smul_smul — Mathlib

English

Two left-invariant measures on a locally compact group that are finite on compacts must be proportional: μ' = haarScalarFactor μ' μ · μ.

Русский

Две левInvariantные меры на локально компактной группе, конечные на компактах, пропорциональны: μ' = haarScalarFactor μ' μ · μ.

LaTeX

$$$$μ' = haarScalarFactor μ' μ \\cdot μ.$$$$

Lean4

@[to_additive addHaarScalarFactor_smul_smul]
theorem haarScalarFactor_smul_smul [LocallyCompactSpace G] (μ' μ : Measure G) [IsHaarMeasure μ]
    [IsFiniteMeasureOnCompacts μ'] [IsMulLeftInvariant μ'] {c : ℝ≥0} (hc : c ≠ 0) :
    haveI : IsHaarMeasure (c • μ) := IsHaarMeasure.nnreal_smul _ hc
    haarScalarFactor (c • μ') (c • μ) = haarScalarFactor μ' μ :=
  by rw [haarScalarFactor_smul, smul_eq_mul, mul_haarScalarFactor_smul _ _ hc]

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