Commit 2021-01-16 21:37 787e6b30

feat(measure_theory/haar_measure): Prove uniqueness (#5663) Prove the uniqueness of Haar measure (up to a scalar) following Measure Theory by Paul Halmos. This proof seems to contain an omission which we fix by adding an extra hypothesis to an intermediate lemma. Add some lemmas about left invariant regular measures. We add the file measure_theory.prod_group which contain various measure-theoretic properties of products of topological groups, needed for the uniqueness. We add @[to_additive] to some declarations in measure_theory, but leave it out for many because of #4210. This causes some renamings in concepts, like is_left_invariant -> is_mul_left_invariant and measure.conj -> measure.inv (though a better naming suggestion for this one is welcome).