mathlib

fc4e471b - feat(measure_theory/group/basic): make is_[add|mul]_[left|right]_invariant classes (#11655)

feat(measure_theory/group/basic): make is_[add|mul]_[left|right]_invariant classes (#11655) * Simplify the definitions of these classes * Generalize many results about topological groups to measurable groups (still to do in `group/prod`) * Simplify some proofs * Make function argument of `integral_mul_[left|right]_eq_self` explicit (otherwise it is hard to apply this lemma in case the function is not a variable) Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>