Carleson/ToMathlib/MeasureTheory/Measure/Haar/Unique.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)
Imported by 2 files
  1. instance MeasureTheory.Measure.(instance at line 21) line 21 source

    Source documentation

    Any regular bi-invariant additive Haar measure is invariant under negation.

    instance (priority := 100) IsHaarMeasure.isInvInvariant_of_isMulRightInvariant (μ : Measure G)
…
  2. instance MeasureTheory.Measure.(instance at line 51) line 51 source