Commit 2023-11-29 14:38 722e62ad
View on Github →feat: uniqueness of Haar measure in general locally compact groups (#8198)
We prove that two regular Haar measures in a locally compact group coincide up to scalar multiplication, and the same thing for inner regular Haar measures. This is implemented in a new file MeasureTheory.Measure.Haar.Unique. A few results that used to be in the MeasureTheory.Measure.Haar.Basic are moved to this file (and extended) so several imports have to be changed.