Commit 2021-09-23 14:08 cc0d8391

feat(measure_theory/measure/haar): cleanup, link with the is_haar_measure typeclass (#9244) We show that the Haar measure constructed in measure_theory/measure/haar satisfies the is_haar_measure typeclass, and use the existence to show a few further properties of all Haar measures. Also weaken a little bit some assumptions in this file.