Theorem MeasureTheory.Measure.exists_integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport

Modification history

2024-02-14 00:27

Mathlib/MeasureTheory/Measure/Haar/Unique.lean

feat: better uniqueness results for the Haar measure (#9909) …

Modified MeasureTheory.Measure.exists_integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport View on Github →

2024-01-18 09:44

Mathlib/MeasureTheory/Measure/Haar/Unique.lean

feat: construct Haar measure in locally compact non-Hausdorff groups (#9746) …

Added MeasureTheory.Measure.exists_integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport View on Github →