mathlib3

10079b92 - feat(measure_theory/group/action): `smul_invariant_measure` instances (#17590)

feat(measure_theory/group/action): `smul_invariant_measure` instances (#17590) These three instances were used locally in `measure_theory.measure.haar_quotient`. Make them instances, generalize and move to `measure_theory.group.action`. Neither `is_mul_left_invariant`/`is_mul_right_invariant` and `smul_invariant_measure` imported each other. Here I am deciding that the latter would import the former, similar to how actions import groups. Co-authored-by: Oliver Nash <github@olivernash.org>