mathlib3

ec247d43 - feat(measure_theory/group/prod): add properties for right-invariant measures (#16913)

feat(measure_theory/group/prod): add properties for right-invariant measures (#16913) * Use `measure_preserving` more in `measure_theory.group.measure`. * Add instance `is_haar_measure.is_inv_invariant` for abelian groups; remove two (unused) lemmas that are a consequence of this. * Improve docstrings in `measure_theory.group.prod` * Sort the file `measure_theory.group.prod` now in sections `left_invariant`, `right_invariant`, `quasi_measure_preserving` * Continuation of #16668 * Part of #16706