Commit 2025-12-04 09:22 d257f215

View on Github →

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

Estimated changes

Modified Mathlib/Algebra/Polynomial/Factors.lean

added theorem Polynomial.Splits.dvd_iff_roots_le_roots

added theorem Polynomial.Splits.dvd_of_roots_le_roots

added theorem Polynomial.Splits.eq_prod_roots_of_monic

added theorem Polynomial.Splits.image_rootSet

added theorem Polynomial.Splits.map_roots

Modified Mathlib/Algebra/Polynomial/Splits.lean

deleted theorem Polynomial.Splits.dvd_iff_roots_le_roots

deleted theorem Polynomial.Splits.dvd_of_roots_le_roots

deleted theorem Polynomial.eq_prod_roots_of_monic_of_splits_id

deleted theorem Polynomial.image_rootSet

deleted theorem Polynomial.roots_map

deleted theorem Polynomial.splits_of_exists_multiset

Modified Mathlib/FieldTheory/AbelRuffini.lean

Modified Mathlib/FieldTheory/Finite/Basic.lean

Modified Mathlib/FieldTheory/Galois/Basic.lean

Modified Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean

Modified Mathlib/FieldTheory/KummerExtension.lean

Modified Mathlib/FieldTheory/Normal/Basic.lean

Modified Mathlib/FieldTheory/PolynomialGaloisGroup.lean

Modified Mathlib/FieldTheory/SeparableDegree.lean

Modified Mathlib/FieldTheory/SplittingField/IsSplittingField.lean

Modified Mathlib/RingTheory/Adjoin/Field.lean

Modified Mathlib/RingTheory/Polynomial/Resultant/Basic.lean