Choice of notation for convolution of measures

Stream: mathlib4

[Josha Dekker]

Hi, in #9372 I've defined the (multiplicative- and additive-) convolution of measures. I think that it makes sense to use * for additive convolution, but I'm a bit worried about using the same thing for multiplicative convolution: if the underlying space is a additive AND a multiplicative monoid, * could then refer to either convolution, which I feel like might lead to undesirable confusion down the road...