mathlib

214a80f3 - feat(data/mv_polynomial/variables): API for mv_polynomial.degree_of (#10646)

feat(data/mv_polynomial/variables): API for mv_polynomial.degree_of (#10646) This PR provides some API for `mv_polynomial.degree_of` for `comm_ring` and `comm_semiring`. I don't know which of these lemmas should be simp lemmas. Co-authored-by: Iván Sadofschi Costa <isadofschi@users.noreply.github.com>