Theorems · Definition · measure theory

MeasureTheory.mulEquivHaarChar

{G : Type u_1} →
  [inst : Group G] →
    [inst_1 : TopologicalSpace G] →
      [inst_2 : MeasurableSpace G] →
        [BorelSpace G] → [IsTopologicalGroup G] → [LocallyCompactSpace G] → G ≃ₜ* G → NNReal

If φ : G ≃ₜ* G then mulEquivHaarChar φ is the positive real factor by which φ scales Haar measures on G.

Defined in

Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar

Cited by

12 results in Mathlib

Foundations

Depth 271 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupTopologicalSpaceMeasurableSpaceBorelSpaceIsTopologicalGroupLocallyCompactSpace