mathlib

a8831524 - doc(data/mv_polynomial/basic): Fix documentation of mv_polynomial.monomial (#5160)

doc(data/mv_polynomial/basic): Fix documentation of mv_polynomial.monomial (#5160) The documenting comment for this function was obviously lifted from the single variable polynomial version, and did not make sense. I'm not sure if this is the right comment, but it is at least better to what it was before.