mathlib3

4b83fd28 - feat(measure_theory/group.measure): add pi.is_haar_measure (#18390)

feat(measure_theory/group.measure): add pi.is_haar_measure (#18390) Add the proof that a finite product of Haar measures is a Haar measure by proving the following instances `pi.is_open_pos_measure` and `pi.is_finite_measure_on_compacts` It is also necessary to prove a lemma `is_open_pi_iff` belonging to an already ported file. The corresponding mathlib4 PR is: https://github.com/leanprover-community/mathlib4/pull/2110 Co-authored-by: Eric Wieser <wieser.eric@gmail.com>