Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-28 22:58 6d3e9362

View on Github →

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).

Estimated changes

modified theorem finset.ae_measurable_prod'
modified theorem finset.ae_measurable_prod
modified theorem finset.measurable_prod'
modified theorem finset.measurable_prod
modified theorem list.ae_measurable_prod'
modified theorem list.ae_measurable_prod
modified theorem list.measurable_prod'
modified theorem list.measurable_prod
modified theorem multiset.ae_measurable_prod
modified theorem multiset.measurable_prod'
modified theorem multiset.measurable_prod