Convolution of sequences in semirings

[malarbol]

This PR introduces the convolution product of sequences in (semi)rings.

More precisely, it introduces the following concepts:

• sequences-semirings: semirings of sequences in semirings with pointwise addition and multiplication;
• sequences-rings: rings of sequences in rings with pointwise addition and multiplication;
• dirac-sequences-semirings: sequences δ : ℕ → ℕ → R such that δ i i ＝ 1 and δ i j ＝ 0 for i ≠ j;
• convolution-sequence-semirings: semirings of sequences in semirings with pointwise addition and convolution product;
• convolution-sequence-rings: rings of sequences in rings with pointwise addition and convolution product.

Most of the proofs are adapted from the current definitions of convolution in commutative (semi)rings. Conversely, these current definitions are refactored to use the new concepts.

[malarbol]

This is intended as a first step towards the definition of the exponential series in ring extensions of ℚ. (c.f. https://github.com/UniMath/agda-unimath/pull/1747/changes#r2594513731)

[malarbol]

I renamed a few concepts introduced by @lowasser. E.g. the convolution product is now called mul-convolution-sequence-Ring and convolution-sequence-Ring is now the Ring of sequences under convolution. I hope it's ok.