Commit 2025-09-23 12:05 a3f0fd53

feat(MeasureTheory): Convolution of diracs (#29826) Add dirac_mconv_dirac which gives a formula for the convolution of diracs. (I made it a simp lemma because I think its a good simp lemma but not totally sure). Also cleaned up the rest of the file by removing unnecessary uses of Measure prefix (since the Measure namespace is open).