Commit 2025-11-21 12:10 21bf164c

View on Github →

refactor(Algebra/Polynomial/Factors): rename Factors to Splits (#31878) This PR renames Factors to Splits. There is still plenty of work to be done in cleaning up Splits.lean, but that can wait for follow-up PRs. The first commit is a direct find & replace, and the rest are manual fixes.

Estimated changes

Modified Mathlib/Algebra/Polynomial/Factors.lean

deleted theorem Polynomial.Factors.C_mul_X_pow

deleted theorem Polynomial.Factors.X_add_C

deleted theorem Polynomial.Factors.X_pow

deleted theorem Polynomial.Factors.X_sub_C

deleted theorem Polynomial.Factors.eq_prod_roots

deleted theorem Polynomial.Factors.exists_eval_eq_zero

deleted theorem Polynomial.Factors.listProd

deleted theorem Polynomial.Factors.monomial

deleted theorem Polynomial.Factors.multisetProd

deleted theorem Polynomial.Factors.natDegree_eq_card_roots

deleted theorem Polynomial.Factors.natDegree_le_one_of_irreducible

deleted theorem Polynomial.Factors.of_degree_eq_one

deleted theorem Polynomial.Factors.of_degree_le_one

deleted theorem Polynomial.Factors.of_dvd

deleted theorem Polynomial.Factors.of_natDegree_eq_one

deleted theorem Polynomial.Factors.of_natDegree_le_one

deleted theorem Polynomial.Factors.roots_ne_zero

deleted theorem Polynomial.Factors.splits

deleted def Polynomial.Factors

added theorem Polynomial.Splits.C_mul_X_pow

added theorem Polynomial.Splits.X_add_C

added theorem Polynomial.Splits.X_pow

added theorem Polynomial.Splits.X_sub_C

added theorem Polynomial.Splits.eq_prod_roots

added theorem Polynomial.Splits.exists_eval_eq_zero

added theorem Polynomial.Splits.listProd

added theorem Polynomial.Splits.monomial

added theorem Polynomial.Splits.multisetProd

added theorem Polynomial.Splits.natDegree_eq_card_roots

added theorem Polynomial.Splits.natDegree_le_one_of_irreducible

added theorem Polynomial.Splits.of_degree_eq_one

added theorem Polynomial.Splits.of_degree_le_one

added theorem Polynomial.Splits.of_dvd

added theorem Polynomial.Splits.of_natDegree_eq_one

added theorem Polynomial.Splits.of_natDegree_le_one

added theorem Polynomial.Splits.roots_ne_zero

added theorem Polynomial.Splits.splits

added def Polynomial.Splits

deleted theorem Polynomial.factors_X_sub_C_mul_iff

deleted theorem Polynomial.factors_iff_exists_multiset'

deleted theorem Polynomial.factors_iff_exists_multiset

deleted theorem Polynomial.factors_iff_splits

deleted theorem Polynomial.factors_mul_iff

deleted theorem Polynomial.factors_neg_iff

deleted theorem Polynomial.factors_of_degree_le_zero

deleted theorem Polynomial.factors_of_natDegree_eq_zero

added theorem Polynomial.splits_X_sub_C_mul_iff

added theorem Polynomial.splits_iff_exists_multiset'

added theorem Polynomial.splits_iff_exists_multiset

added theorem Polynomial.splits_iff_splits

added theorem Polynomial.splits_mul_iff

added theorem Polynomial.splits_neg_iff

added theorem Polynomial.splits_of_degree_le_zero

added theorem Polynomial.splits_of_natDegree_eq_zero

Modified Mathlib/Algebra/Polynomial/Splits.lean

deleted def Polynomial.Splits

deleted theorem Polynomial.splits_iff_exists_multiset

deleted theorem Polynomial.splits_mul_iff

Modified Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean

Modified Mathlib/FieldTheory/AbelRuffini.lean

Modified Mathlib/FieldTheory/IsAlgClosed/Basic.lean

Modified Mathlib/FieldTheory/IsSepClosed.lean

Modified Mathlib/FieldTheory/Separable.lean

Modified Mathlib/FieldTheory/SeparableDegree.lean

Modified Mathlib/RingTheory/Polynomial/IsIntegral.lean

Modified Mathlib/RingTheory/Polynomial/ScaleRoots.lean

modified theorem Polynomial.Factors.scaleRoots