In [13.1](https://leanprover-community.github.io/mathematics_in_lean/C13_Integration_and_Measure_Theory.html#elementary-integration), it should be pointed out that the symbols for convolution and for multiplication are different (because they look very similar).