Commit 2025-11-25 07:17 786ca91a

View on Github →

feat(RingTheory): resultant is multiplicative (#31871)

Estimated changes

Modified Mathlib/Algebra/Polynomial/Factors.lean

added theorem Polynomial.Splits.taylor

added theorem Polynomial.map_sub_roots_sprod_eq_prod_map_eval

added theorem Polynomial.map_sub_sprod_roots_eq_prod_map_eval

Modified Mathlib/Algebra/Polynomial/Taylor.lean

added theorem Polynomial.map_taylor

Modified Mathlib/RingTheory/Polynomial/Resultant/Basic.lean

added theorem Polynomial.resultant_X_add_C_left

added theorem Polynomial.resultant_X_add_C_right

added theorem Polynomial.resultant_X_pow_left

added theorem Polynomial.resultant_X_pow_right

modified theorem Polynomial.resultant_X_sub_C_left

added theorem Polynomial.resultant_X_sub_C_pow_left

added theorem Polynomial.resultant_X_sub_C_pow_right

modified theorem Polynomial.resultant_X_sub_C_right

added theorem Polynomial.resultant_dvd_leadingCoeff_pow

added theorem Polynomial.resultant_eq_prod_roots_sub

added theorem Polynomial.resultant_integralNormalization

added theorem Polynomial.resultant_mul_left

added theorem Polynomial.resultant_ne_zero

added theorem Polynomial.resultant_pow_left

added theorem Polynomial.resultant_pow_right

added theorem Polynomial.resultant_prod_left

added theorem Polynomial.resultant_prod_right

added theorem Polynomial.resultant_self_eq_zero

Modified Mathlib/RingTheory/Polynomial/ScaleRoots.lean

deleted theorem Polynomial.Factors.scaleRoots

added theorem Polynomial.Splits.scaleRoots