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.