feat(measure_theory): add @[to_additive] (#8142)
This PR adds `@[to_additive]` to `haar_measure` and everything that depends on. This will allow us to define the Lebesgue measure on `ℝ` and `ℝ ^ n` as the Haar measure (or just show that it is equal to it).
Co-authored-by: Floris van Doorn <fpv@andrew.cmu.edu>
