Theorem MeasureTheory.Measure.ext_of_lintegral

Modification history

2025-03-25 10:42
Mathlib/MeasureTheory/Integral/Lebesgue.lean
feat(MeasureTheory): add API to convolution of measures and lintegrals (#23292) …
Added MeasureTheory.Measure.ext_of_lintegralView on Github →