Theorem MeasureTheory.Measure.mconv_dirac_one

Modification history

2024-02-17 18:52
Mathlib/MeasureTheory/Group/Convolution.lean
Convolution of measures (#9372) …
Added MeasureTheory.Measure.mconv_dirac_oneView on Github →