Commit 2024-02-14 00:27 5efaaf85
View on Github →feat: better uniqueness results for the Haar measure (#9909) We show that two Haar measures give the same measure to sets with compact closure, and to open sets, without any regularity assumptions. This is based on McQuillan's answer on https://mathoverflow.net/questions/456670.
Estimated changes
modified theorem MeasureTheory.Measure.exists_integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport
added theorem MeasureTheory.Measure.measure_isMulInvariant_eq_smul_of_isCompact_closure_of_innerRegularCompactLTTop
added theorem MeasureTheory.Measure.measure_isMulInvariant_eq_smul_of_isCompact_closure_of_measurableSet