isHaarMeasure_map_mul_right — Mathlib

English

A Haar measure image under a multiplicative equivalence is Haar.

Русский

Образ меры Хаара под мультиэквивалентом сохраняет хар-ку Хаара.

LaTeX

$$$\text{MulEquiv.isHaarMeasureMap}(μ, e)$$$

Lean4

/-- The image of a Haar measure under right multiplication is again a Haar measure. -/
@[to_additive isHaarMeasure_map_add_right /--
    The image of a Haar measure under right addition is again a Haar measure. -/
    ]
instance isHaarMeasure_map_mul_right [BorelSpace G] [IsTopologicalGroup G] (g : G) :
    IsHaarMeasure (Measure.map (· * g) μ) :=
  isHaarMeasure_map_smul μ (MulOpposite.op g)

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