Unimodular groups

TheoremRight-invariant Haar measures are inversion-invariant#✓fully proved

A right-invariant Haar measure is invariant under inversion.

theorem MeasureTheory.Measure.isInvInvariant_of_isMulRightInvariant
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G]
    [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology G]
    (μ : Measure G) [μ.IsHaarMeasure] [μ.IsMulRightInvariant] : μ.IsInvInvariant

Used by 1

Used byHaar measures on GL(2, F) are right- and inversion-invariant

TheoremGL(2, F) is unimodular#✓fully proved

The modular character of GL (2, F) is trivial: GL (2, F) is unimodular.

theorem modularCharacter_fin_two_eq_one
    {F : Type*} [Field F] [TopologicalSpace F] [IsTopologicalRing F]
    [LocallyCompactSpace (GL (Fin 2) F)] (g : GL (Fin 2) F) :
    MeasureTheory.Measure.modularCharacter g = 1

Used by 1

Used byHaar measures on GL(2, F) are right- and inversion-invariant

TheoremHaar measures on GL(2, F) are right- and inversion-invariant#✓fully proved

Every Haar measure on GL (2, F) is right-invariant and inversion-invariant.

theorem isMulRightInvariant_and_isInvInvariant_of_isHaarMeasure_fin_two
    {F : Type*} [Field F] [TopologicalSpace F] [IsTopologicalRing F]
    [LocallyCompactSpace (GL (Fin 2) F)] [SecondCountableTopology (GL (Fin 2) F)]
    [MeasurableSpace (GL (Fin 2) F)] [BorelSpace (GL (Fin 2) F)]
    (μ : MeasureTheory.Measure (GL (Fin 2) F)) [μ.IsHaarMeasure] :
    μ.IsMulRightInvariant ∧ μ.IsInvInvariant

Uses 2

Proof usesGL(2, F) is unimodular · Right-invariant Haar measures are inversion-invariant

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.