Commit 2024-11-28 14:24 061f06f3

View on Github →

feat: Polynomial.isRoot_of_isRoot_iff_dvd_derivative_mul (#19146)

Estimated changes

Modified Mathlib/Algebra/Polynomial/FieldDivision.lean

added theorem Polynomial.isRoot_of_isRoot_of_dvd_derivative_mul

Modified Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean

added theorem Polynomial.isRoot_of_isRoot_iff_dvd_derivative_mul