Theorems · Definition · Lie groups

MeasureTheory.Measure.addModularCharacterFun

{G : Type u_1} →
  [inst : TopologicalSpace G] → [inst_1 : AddGroup G] → [IsTopologicalAddGroup G] → [LocallyCompactSpace G] → G → NNReal

The additive modular character as a map is g ↦ μ (· - g) / μ, where μ is an left additive Haar measure.

Defined in

Mathlib.MeasureTheory.Group.ModularCharacter

Cited by

5 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceAddGroupIsTopologicalAddGroupLocallyCompactSpace