Notation for (Add)MonoidAlgebra

Stream: mathlib4

[Jz Pan]

Currently the notation for docs#AddMonoidAlgebra is R[G], while there is no notation for docs#MonoidAlgebra. Do R[G] conflicts with the polynomial notation R[X]?

I propose the change of the notation of docs#AddMonoidAlgebra to R[⁺G], while the notation for docs#MonoidAlgebra should be R[ˣG]. Do you think it's a good idea?

[Jz Pan]

This should not conflict with the notation Rˣ for docs#Units.