Theorem MeasureTheory.Measure.ext_iff_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_iff_lintegralView on Github →