Theorems · Definition · measure theory

MeasureTheory.addEquivAddHaarChar

{G : Type u_1} →
  [inst : AddGroup G] →
    [inst_1 : TopologicalSpace G] →
      [inst_2 : MeasurableSpace G] →
        [BorelSpace G] → [IsTopologicalAddGroup G] → [LocallyCompactSpace G] → G ≃ₜ+ G → NNReal

If φ : A ≃ₜ+ A then addEquivAddHaarChar φ is the positive real factor by which φ scales Haar measures on A.

Defined in

Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar

Cited by

11 results in Mathlib

Foundations

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

Assumes

AddGroupTopologicalSpaceMeasurableSpaceBorelSpaceIsTopologicalAddGroupLocallyCompactSpace