Commit 2022-10-13 20:27 ec247d43

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