Theorems · Definition · Lie groups

MeasureTheory.Measure.modularCharacterFun

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

The modular character as a map is g ↦ μ (· * g⁻¹) / μ, where μ is a left Haar measure. See also modularCharacter that defines the map as a homomorphism.

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

TopologicalSpaceGroupIsTopologicalGroupLocallyCompactSpace