mathlib

4daac664 - chore(field_theory/mv_polynomial): generalised to comm_ring and module doc (#6341)

chore(field_theory/mv_polynomial): generalised to comm_ring and module doc (#6341) This PR generalises most of `field_theory/mv_polynomial` from polynomial rings over fields to polynomial rings over commutative rings. This is put into a separate file. Also renamed the field to K and did one tiny golf. Co-authored-by: Julian-Kuelshammer <68201724+Julian-Kuelshammer@users.noreply.github.com>