Theorem MeasureTheory.Measure.zero_mconv

Modification history

2025-06-05 11:52
Mathlib/MeasureTheory/Group/Convolution.lean
feat(MeasureTheory): Distinct Notation for Multiplicative and Additive Convolution (#25434) …
Modified MeasureTheory.Measure.zero_mconvView on Github →
2025-03-25 10:42
Mathlib/MeasureTheory/Group/Convolution.lean
feat(MeasureTheory): add API to convolution of measures and lintegrals (#23292) …
Modified MeasureTheory.Measure.zero_mconvView on Github →
2024-02-17 18:52
Mathlib/MeasureTheory/Group/Convolution.lean
Convolution of measures (#9372) …
Added MeasureTheory.Measure.zero_mconvView on Github →