mulEquivHaarChar_smul_map — Mathlib

English

For a Haar measure μ and φ, scaling the pushforward measure by mulEquivHaarChar φ recovers μ: mulEquivHaarChar φ · μ.map φ = μ.

Русский

Для меры Хаара μ и φ масштабирование на mulEquivHaarChar φ возвращает исходную меру: mulEquivHaarChar φ · μ.map φ = μ.

LaTeX

$$$mulEquivHaarChar(\phi) \cdot μ.map φ = μ$$$

Lean4

@[to_additive addEquivAddHaarChar_smul_map]
theorem mulEquivHaarChar_smul_map (μ : Measure G) [IsHaarMeasure μ] [Regular μ] (φ : G ≃ₜ* G) :
    mulEquivHaarChar φ • μ.map φ = μ := by
  rw [mulEquivHaarChar_eq μ φ]
  have : Regular (map φ μ) := Regular.map φ.toHomeomorph
  exact (isMulLeftInvariant_eq_smul_of_regular μ (map φ μ)).symm

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