mathlib

c99203f7 - feat(measure_theory/integral/interval_integral): add lemmas (#16986)

feat(measure_theory/integral/interval_integral): add lemmas (#16986) * Clean up some implicit arguments * Slightly generalize `continuous_linear_map.interval_integral_comp_comm` * From the sphere eversion project Co-authored by: Patrick Massot [patrick.massot@u-psud.fr](mailto:patrick.massot@u-psud.fr)