Theorem Polynomial.nextCoeff_eq_neg_sum_roots_mul_leadingCoeff_of_splits

Modification history

2025-12-12 09:27
Mathlib/Algebra/Polynomial/Splits.lean
refactor(Algebra/Polynomial/Splits): continue deprecation (#32752) …
Deleted Polynomial.nextCoeff_eq_neg_sum_roots_mul_leadingCoeff_of_splitsView on Github →
2025-11-20 19:42
Mathlib/Algebra/Polynomial/Splits.lean
feat(Algebra/Polynomial/Splits): remove the `RingHom` argument of `Splits` (#31631)
Modified Polynomial.nextCoeff_eq_neg_sum_roots_mul_leadingCoeff_of_splitsView on Github →
2025-11-05 17:11
Mathlib/Algebra/Polynomial/Splits.lean
feat(Algebra/Polynomial): small and useful lemmas (#29956)
Added Polynomial.nextCoeff_eq_neg_sum_roots_mul_leadingCoeff_of_splitsView on Github →