Theorem Polynomial.coeff_zero_eq_leadingCoeff_mul_prod_roots_of_splits

Modification history

2025-12-12 09:27
Mathlib/Algebra/Polynomial/Splits.lean
refactor(Algebra/Polynomial/Splits): continue deprecation (#32752) …
Deleted Polynomial.coeff_zero_eq_leadingCoeff_mul_prod_roots_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.coeff_zero_eq_leadingCoeff_mul_prod_roots_of_splitsView on Github →
2025-11-05 17:11
Mathlib/Algebra/Polynomial/Splits.lean
feat(Algebra/Polynomial): small and useful lemmas (#29956)
Added Polynomial.coeff_zero_eq_leadingCoeff_mul_prod_roots_of_splitsView on Github →