Theorems · Theorem · measure theory

MeasureTheory.distribHaarChar_apply

∀ {G : Type u_1} (A : Type u_2) [inst : Group G] [inst_1 : AddCommGroup A] [inst_2 : DistribMulAction G A]
  [inst_3 : TopologicalSpace A] [inst_4 : IsTopologicalAddGroup A] [inst_5 : LocallyCompactSpace A]
  [inst_6 : ContinuousConstSMul G A] (g : G),
  (MeasureTheory.distribHaarChar A) g =
    (DomMulAct.mk g • MeasureTheory.Measure.addHaar).addHaarScalarFactor MeasureTheory.Measure.addHaar

Defined in

Mathlib.MeasureTheory.Measure.Haar.DistribChar

Cited by

0 results in Mathlib

Foundations

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

Assumes

GroupAddCommGroupDistribMulActionTopologicalSpaceIsTopologicalAddGroupLocallyCompactSpaceContinuousConstSMul