Contrary to the case of polynomials and multivariate polynomials, this does not look so useful and I prefer to close it now.

I'd be tempted to keep this because it provides the multivariate polynomial version for free.

The point is that all functions are trivial in this case. What makes the case of multivariate polynomials interesting is the relation with coefficients, MvPolynomial.sum, etc.

OK, coeff and monomial don't exist, but one can “apply”, and use MonoidAlgebra.single to add functions equivalent to what is done for MvPolynomial in #12293 .
The initial lemmas have been commented out and one of them is done explicitly, I should restore something because this half-functoriality of MonoidAlgebra is important and playing with liftNC all the time is painful.

Are you still working on this? It looks like this duplicates #29539 from Toric.

No, I'm not. We really needed the MvPolynomial part, which we did, and I felt we had to do the analogues (MonoidAlgebra, Polynomial), but since they weren't used and nobody had a look, we left it rot.