Commit 2025-12-01 09:24 d6cf3d86

View on Github →

refactor(Algebra/Polynomial/Splits): continue deprecation (#32284) 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

modified theorem Polynomial.Splits.comp_X_sub_C

added theorem Polynomial.Splits.degree_eq_card_roots

added theorem Polynomial.Splits.degree_eq_one_of_irreducible

added theorem Polynomial.Splits.degree_le_one_of_irreducible

added theorem Polynomial.Splits.natDegree_eq_one_of_irreducible

added theorem Polynomial.splits_iff_card_roots

added theorem Polynomial.splits_prod_iff

Modified Mathlib/Algebra/Polynomial/Splits.lean

deleted theorem Polynomial.Splits.def

deleted theorem Polynomial.degree_eq_card_roots

deleted theorem Polynomial.degree_eq_one_of_irreducible_of_splits

deleted theorem Polynomial.natDegree_eq_card_roots

deleted theorem Polynomial.splits_iff

deleted theorem Polynomial.splits_iff_card_roots

deleted theorem Polynomial.splits_of_splits_id

deleted theorem Polynomial.splits_prod_iff

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

Modified Mathlib/FieldTheory/AbelRuffini.lean

Modified Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean

Modified Mathlib/FieldTheory/IsAlgClosed/Basic.lean

Modified Mathlib/FieldTheory/IsSepClosed.lean

Modified Mathlib/FieldTheory/Normal/Defs.lean

Modified Mathlib/FieldTheory/PrimitiveElement.lean

Modified Mathlib/FieldTheory/Separable.lean