Commit 2025-12-02 09:53 d42cf401

View on Github →

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

Estimated changes

Modified Archive/Wiedijk100Theorems/AbelRuffini.lean

Modified Mathlib/Algebra/Polynomial/Factors.lean

added theorem Polynomial.eval_rootOfSplits

Modified Mathlib/Algebra/Polynomial/Splits.lean

deleted theorem Polynomial.degree_eq_card_roots'

deleted theorem Polynomial.exists_root_of_splits'

deleted theorem Polynomial.exists_root_of_splits

deleted theorem Polynomial.map_rootOfSplits'

deleted theorem Polynomial.map_rootOfSplits

deleted theorem Polynomial.natDegree_eq_card_roots'

deleted def Polynomial.rootOfSplits'

deleted def Polynomial.rootOfSplits

deleted theorem Polynomial.roots_ne_zero_of_splits'

deleted theorem Polynomial.roots_ne_zero_of_splits

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

Modified Mathlib/FieldTheory/AbelRuffini.lean

Modified Mathlib/FieldTheory/Extension.lean

Modified Mathlib/FieldTheory/IsAlgClosed/Basic.lean

Modified Mathlib/FieldTheory/IsSepClosed.lean

Modified Mathlib/FieldTheory/KummerExtension.lean

Modified Mathlib/FieldTheory/PolynomialGaloisGroup.lean

Modified Mathlib/FieldTheory/SeparableDegree.lean

Modified Mathlib/NumberTheory/Cyclotomic/Basic.lean

Modified Mathlib/RingTheory/Adjoin/Field.lean

Modified Mathlib/Topology/Algebra/Polynomial.lean