Commit 2021-09-08 14:01 146dddc3

View on Github →

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.

Estimated changes

Modified src/algebra/add_torsor.lean

deleted theorem pi.vadd_apply

Modified src/algebra/module/pi.lean

modified theorem pi.smul_apply

Modified src/measure_theory/group/arithmetic.lean

Modified src/measure_theory/measure/haar.lean

added theorem measure_theory.measure.add_haar_measure_apply