Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes