Theorems · Definition · Lie groups

MeasureTheory.Measure.modularCharacter

{G : Type u_1} →
  [inst : TopologicalSpace G] → [inst_1 : Group G] → [IsTopologicalGroup G] → [LocallyCompactSpace G] → G →* NNReal

The modular character homomorphism. The underlying function is modularCharacterFun, which is g ↦ μ (· * g⁻¹) / μ, where μ is a left Haar measure.

Defined in

Mathlib.MeasureTheory.Group.ModularCharacter

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceGroupIsTopologicalGroupLocallyCompactSpace