Commit 2025-12-12 09:27 aef4be2c

View on Github →

refactor(Algebra/Polynomial/Splits): continue deprecation (#32752) This PR continues the deprecation in Splits.lean as we move over to the new API in Factors.lean.

Estimated changes

Modified Mathlib/Algebra/Polynomial/Factors.lean

added theorem Polynomial.Splits.coeff_zero_eq_leadingCoeff_mul_prod_roots

added theorem Polynomial.Splits.coeff_zero_eq_prod_roots_of_monic

added theorem Polynomial.Splits.eval_derivative_div_eval_of_ne_zero

added theorem Polynomial.Splits.eval_derivative_eq_eval_mul_sum

added theorem Polynomial.Splits.nextCoeff_eq_neg_sum_roots_mul_leadingCoeff

added theorem Polynomial.Splits.nextCoeff_eq_neg_sum_roots_of_monic

Modified Mathlib/Algebra/Polynomial/Splits.lean

deleted theorem Polynomial.coeff_zero_eq_leadingCoeff_mul_prod_roots_of_splits

deleted theorem Polynomial.coeff_zero_eq_prod_roots_of_monic_of_splits

deleted theorem Polynomial.eval_derivative_div_eval_of_ne_zero_of_splits

deleted theorem Polynomial.eval_derivative_eq_eval_mul_sum_of_splits

deleted theorem Polynomial.nextCoeff_eq_neg_sum_roots_mul_leadingCoeff_of_splits

deleted theorem Polynomial.nextCoeff_eq_neg_sum_roots_of_monic_of_splits

Modified Mathlib/Analysis/Complex/Polynomial/GaussLucas.lean

Modified Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean

Modified Mathlib/LinearAlgebra/Matrix/Charpoly/Eigs.lean

Modified Mathlib/RingTheory/Norm/Basic.lean

Modified Mathlib/RingTheory/Trace/Basic.lean