Commit 2025-06-05 11:52 7d5bdba1
View on Github →feat(MeasureTheory): Distinct Notation for Multiplicative and Additive Convolution (#25434) Adds distinct notation for additive and multiplicative convolution of measures and lconvolution. This is important when using the notation on types with an additive and multiplicative structure such as $\mathbb{R}$.