Commit 2022-11-29 15:25 10079b92
View on Github →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.