mathlib3

4d79d5fe - chore(measure_theory/group/arithmetic): use implicit argument for measurable_space (#11205)

chore(measure_theory/group/arithmetic): use implicit argument for measurable_space (#11205) The `measurable_space` argument is inferred from other arguments (like `measurable f` or a measure for example) instead of being a type class. This ensures that the lemmas are usable without `@` when several measurable space structures are used for the same type. Also use more `variables`.