theorem ProbabilityTheory.measureConv_dirac_zero : measureConv (MeasureTheory.Measure.dirac 0) (MeasureTheory.Measure.dirac 0) = MeasureTheory.Measure.dirac 0

The convolution of the Dirac measure at 0 with itself is again the Dirac measure at 0: δ₀ ∗ δ₀ = δ₀. A small computational lemma supporting the construction of stable distributions via convolutions.