Commit 2025-11-25 12:35 587e754c

View on Github →

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

Estimated changes

Modified Mathlib/Algebra/Polynomial/Splits.lean

modified theorem Polynomial.Splits.comp_X_add_C

modified theorem Polynomial.Splits.comp_X_sub_C

modified theorem Polynomial.Splits.comp_neg_X

modified theorem Polynomial.Splits.comp_of_degree_le_one

deleted theorem Polynomial.Splits.comp_of_map_degree_le_one

deleted theorem Polynomial.splits_C

deleted theorem Polynomial.splits_X

deleted theorem Polynomial.splits_X_pow

deleted theorem Polynomial.splits_X_sub_C

modified theorem Polynomial.splits_iff_comp_splits_of_degree_eq_one

deleted theorem Polynomial.splits_of_degree_eq_one

deleted theorem Polynomial.splits_of_degree_le_one

deleted theorem Polynomial.splits_of_map_degree_eq_one

modified theorem Polynomial.splits_of_map_eq_C

deleted theorem Polynomial.splits_of_natDegree_eq_one

deleted theorem Polynomial.splits_of_natDegree_le_one

deleted theorem Polynomial.splits_one

deleted theorem Polynomial.splits_pow

deleted theorem Polynomial.splits_prod

deleted theorem Polynomial.splits_zero

Modified Mathlib/FieldTheory/AbelRuffini.lean

Modified Mathlib/FieldTheory/Fixed.lean

Modified Mathlib/FieldTheory/Galois/Basic.lean

Modified Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean

Modified Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean

Modified Mathlib/FieldTheory/IsAlgClosed/Basic.lean

Modified Mathlib/FieldTheory/Isaacs.lean

Modified Mathlib/FieldTheory/KummerExtension.lean

Modified Mathlib/FieldTheory/Normal/Basic.lean

Modified Mathlib/FieldTheory/Normal/Defs.lean

Modified Mathlib/FieldTheory/PolynomialGaloisGroup.lean

Modified Mathlib/FieldTheory/PurelyInseparable/Basic.lean

Modified Mathlib/FieldTheory/SplittingField/Construction.lean

Modified Mathlib/FieldTheory/SplittingField/IsSplittingField.lean

Modified Mathlib/RingTheory/Adjoin/Field.lean

Modified Mathlib/RingTheory/Invariant/Basic.lean