Commit 2025-11-28 14:12 ba5f5106

View on Github →

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

Estimated changes

Modified Mathlib/Algebra/CubicDiscriminant.lean

Modified Mathlib/Algebra/Polynomial/Factors.lean

added theorem IsUnit.splits

added theorem Polynomial.Splits.comp_X_add_C

added theorem Polynomial.Splits.comp_X_sub_C

added theorem Polynomial.Splits.comp_of_degree_le_one

added theorem Polynomial.Splits.comp_of_degree_le_one_of_invertible

added theorem Polynomial.Splits.comp_of_degree_le_one_of_monic

added theorem Polynomial.Splits.comp_of_natDegree_le_one

added theorem Polynomial.Splits.comp_of_natDegree_le_one_of_invertible

added theorem Polynomial.Splits.comp_of_natDegree_le_one_of_monic

deleted theorem Polynomial.Splits.of_dvd

added theorem Polynomial.Splits.splits_of_dvd

added theorem Polynomial.splits_iff_comp_splits_of_degree_eq_one

added theorem Polynomial.splits_iff_comp_splits_of_natDegree_eq_one

added theorem Polynomial.splits_of_degree_le_one_of_invertible

added theorem Polynomial.splits_of_degree_le_one_of_monic

added theorem Polynomial.splits_of_natDegree_le_one_of_invertible

added theorem Polynomial.splits_of_natDegree_le_one_of_monic

Modified Mathlib/Algebra/Polynomial/Splits.lean

deleted theorem Polynomial.Splits.comp_X_add_C

deleted theorem Polynomial.Splits.comp_X_sub_C

deleted theorem Polynomial.Splits.comp_of_degree_le_one

deleted theorem Polynomial.eq_prod_roots_of_splits

deleted theorem Polynomial.eq_prod_roots_of_splits_id

deleted theorem Polynomial.splits_iff_comp_splits_of_degree_eq_one

deleted theorem Polynomial.splits_mul

deleted theorem Polynomial.splits_of_isUnit

deleted theorem Polynomial.splits_of_splits_mul'

deleted theorem Polynomial.splits_of_splits_mul

deleted theorem Polynomial.splits_of_splits_of_dvd

Modified Mathlib/Analysis/Polynomial/MahlerMeasure.lean

Modified Mathlib/FieldTheory/AbelRuffini.lean

Modified Mathlib/FieldTheory/Finite/GaloisField.lean

Modified Mathlib/FieldTheory/Galois/Basic.lean

Modified Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean

Modified Mathlib/FieldTheory/IsAlgClosed/Basic.lean

Modified Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean

Modified Mathlib/FieldTheory/Isaacs.lean

Modified Mathlib/FieldTheory/Normal/Basic.lean

Modified Mathlib/FieldTheory/Normal/Closure.lean

Modified Mathlib/FieldTheory/Normal/Defs.lean

Modified Mathlib/FieldTheory/PolynomialGaloisGroup.lean

Modified Mathlib/FieldTheory/Separable.lean

Modified Mathlib/FieldTheory/SplittingField/IsSplittingField.lean

Modified Mathlib/NumberTheory/Cyclotomic/Basic.lean

Modified Mathlib/RingTheory/Adjoin/Field.lean

Modified Mathlib/RingTheory/Invariant/Basic.lean

Modified Mathlib/RingTheory/Polynomial/IsIntegral.lean