Theorem Polynomial.aeval_eq_prod_aroots_sub_of_monic_of_splits

Modification history

2025-12-08 06:22
Mathlib/Algebra/Polynomial/Splits.lean
refactor(Algebra/Polynomial/Splits): continue deprecation (#32500) …
Deleted Polynomial.aeval_eq_prod_aroots_sub_of_monic_of_splitsView on Github →
2024-09-10 12:58
Mathlib/Algebra/Polynomial/Splits.lean
feat(Algebra/Polynomial/Splits): show that evaluating a split polynomial is the same as looking at the product of the roots (#16601)
Added Polynomial.aeval_eq_prod_aroots_sub_of_monic_of_splitsView on Github →