Commit 2023-03-29 05:49 e94327c0

View on Github →

feat: port RingTheory.Polynomial.Vieta (#3137)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Polynomial/RingDivision.lean

added theorem Polynomial.C_leadingCoeff_mul_prod_multiset_X_sub_C

deleted theorem Polynomial.c_leadingCoeff_mul_prod_multiset_X_sub_C

Modified Mathlib/Data/Polynomial/Splits.lean

Created Mathlib/RingTheory/Polynomial/Vieta.lean

added theorem Finset.prod_X_add_C_coeff

added theorem Multiset.esymm_neg

added theorem Multiset.prod_X_add_C_coeff'

added theorem Multiset.prod_X_add_C_coeff

added theorem Multiset.prod_X_add_C_eq_sum_esymm

added theorem Multiset.prod_X_sub_C_coeff

added theorem Multiset.prod_X_sub_X_eq_sum_esymm

added theorem MvPolynomial.prod_C_add_X_eq_sum_esymm

added theorem MvPolynomial.prod_X_add_C_coeff

added theorem Polynomial.coeff_eq_esymm_roots_of_card

added theorem Polynomial.coeff_eq_esymm_roots_of_splits