lebesgue): use to_additive when declaring instances and basic lemmas about simple functions (#12000)

Commit

3 years ago

chore(measure_theory/integral/lebesgue): use to_additive when declaring instances and basic lemmas about simple functions (#12000) I also grouped similar lemmas together and added one or two missing ones.

Author

RemyDegenne

Parents

4b217ea7

mathlib af1355c4 - chore(measure_theory/integral/lebesgue): use to_additive when declaring instances and basic lemmas about simple functions (#12000)

mathlib
af1355c4 - chore(measure_theory/integral/lebesgue): use to_additive when declaring instances and basic lemmas about simple functions (#12000)