Theorems · Theorem · Lie groups

MeasureTheory.Measure.map_right_mul_eq_modularCharacterFun_smul

∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : LocallyCompactSpace G] [inst_4 : MeasurableSpace G] [BorelSpace G] (μ : MeasureTheory.Measure G)
  [μ.IsHaarMeasure] [μ.InnerRegular] (g : G),
  MeasureTheory.Measure.map (fun x => x * g) μ = MeasureTheory.Measure.modularCharacterFun g • μ

Defined in: Mathlib.MeasureTheory.Group.ModularCharacter
Cited by: 0 results in Mathlib
Foundations: Depth 279 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: TopologicalSpace Group IsTopologicalGroup LocallyCompactSpace MeasurableSpace BorelSpace MeasureTheory.Measure.IsHaarMeasure MeasureTheory.Measure.InnerRegular

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites15

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

TopologicalSpacestatement and proof · cited by 24,529
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
ENNRealstatement · cited by 9,879
Groupstatement and proof · cited by 6,238
NNRealstatement and proof · cited by 4,310
BorelSpacestatement and proof · cited by 1,602
MeasureTheory.Measure.mapstatement and proof · cited by 858
IsTopologicalGroupstatement and proof · cited by 469
LocallyCompactSpacestatement and proof · cited by 324
MeasureTheory.Measure.IsHaarMeasurestatement and proof · cited by 63
MeasureTheory.Measure.InnerRegularstatement and proof · cited by 49

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.