Commit 2022-08-20 08:58 8fdec909

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.