mathlib3

146dddc3 - feat(measure_theory/group/arithmetic): add more to_additive attributes for actions (#9032)

feat(measure_theory/group/arithmetic): add more to_additive attributes for actions (#9032) Introduce additivised versions of some more smul classes and corresponding instances and lemmas for different types of (measurable) additive actions.