Redefine the monomial structures in `monalg.v` to inherit their multiplication from `monoidType` in `monoid.v`

[pi8027]

Once it's done for the (semi)ring structures too, it should enable us to unify the notion of multiplication, and we can probably get rid of monom_scope. Then, we can remove the {mmorphism _ -> _} structure in favor of the {multiplicative _ -> _} structure.