mathlib3

8fdec909 - feat(ring_theory/polynomial): Vieta's formula in terms of `polynomial.roots` (#14908)

feat(ring_theory/polynomial): Vieta's formula in terms of `polynomial.roots` (#14908) Specialize `multiset.prod_X_sub_C_coeff` to the root multiset of a split polynomial over an integral domain to derive the familiar Vieta's formula; update *undergrad.yaml*. Make various stylistic improvements to *polynomial/vieta.lean*: most notably, `open polynomial` to be able to omit the prefix in `polynomial.X` and `polynomial.C`. Instead, write `mv_polynomial.X` with the prefix because it's less frequent. Prove miscellaneous lemmas `list.prod_map_neg`, `multiset.prod_map_neg`, `list.map_nth_le` and `multiset.length_to_list`, which are remnants of a previous approach to prove `polynomial.vieta` superseded by #15008. See below/#14908 for the original motivation for introducing them.