Commit 2026-01-04 12:40 16635ad4

View on Github →

refactor(Algebra/Polynomial/Factors): Deprecate file (#32946) This PR finishes the refactor of Splits.lean by moving the new API in Factors.lean back into Splits.lean.

Estimated changes

Modified Mathlib/Algebra/Polynomial/Factors.lean

deleted theorem IsUnit.splits

deleted theorem Polynomial.Splits.C_mul_X_pow

deleted theorem Polynomial.Splits.X_add_C

deleted theorem Polynomial.Splits.X_pow

deleted theorem Polynomial.Splits.X_sub_C

deleted theorem Polynomial.Splits.adjoin_rootSet_eq_range

deleted theorem Polynomial.Splits.aeval_eq_prod_aroots

deleted theorem Polynomial.Splits.aeval_eq_prod_aroots_of_monic

deleted theorem Polynomial.Splits.coeff_zero_eq_leadingCoeff_mul_prod_roots

deleted theorem Polynomial.Splits.coeff_zero_eq_prod_roots_of_monic

deleted theorem Polynomial.Splits.comp_X_add_C

deleted theorem Polynomial.Splits.comp_X_sub_C

deleted theorem Polynomial.Splits.comp_neg_X

deleted theorem Polynomial.Splits.comp_of_degree_le_one

deleted theorem Polynomial.Splits.comp_of_degree_le_one_of_invertible

deleted theorem Polynomial.Splits.comp_of_degree_le_one_of_monic

deleted theorem Polynomial.Splits.comp_of_natDegree_le_one

deleted theorem Polynomial.Splits.comp_of_natDegree_le_one_of_invertible

deleted theorem Polynomial.Splits.comp_of_natDegree_le_one_of_monic

deleted theorem Polynomial.Splits.degree_eq_card_roots

deleted theorem Polynomial.Splits.degree_eq_one_of_irreducible

deleted theorem Polynomial.Splits.degree_le_one_of_irreducible

deleted theorem Polynomial.Splits.dvd_iff_roots_le_roots

deleted theorem Polynomial.Splits.dvd_of_roots_le_roots

deleted theorem Polynomial.Splits.eq_X_sub_C_of_single_root

deleted theorem Polynomial.Splits.eq_prod_roots

deleted theorem Polynomial.Splits.eq_prod_roots_of_monic

deleted theorem Polynomial.Splits.eval_derivative

deleted theorem Polynomial.Splits.eval_derivative_div_eval_of_ne_zero

deleted theorem Polynomial.Splits.eval_derivative_eq_eval_mul_sum

deleted theorem Polynomial.Splits.eval_eq_prod_roots

deleted theorem Polynomial.Splits.eval_eq_prod_roots_of_monic

deleted theorem Polynomial.Splits.eval_root_derivative

deleted theorem Polynomial.Splits.exists_eval_eq_zero

deleted theorem Polynomial.Splits.image_rootSet

deleted theorem Polynomial.Splits.listProd

deleted theorem Polynomial.Splits.map_roots

deleted theorem Polynomial.Splits.mem_lift_of_roots_mem_range

deleted theorem Polynomial.Splits.mem_range_of_isRoot

deleted theorem Polynomial.Splits.mem_subfield_of_isRoot

deleted theorem Polynomial.Splits.monomial

deleted theorem Polynomial.Splits.multisetProd

deleted theorem Polynomial.Splits.natDegree_eq_card_roots

deleted theorem Polynomial.Splits.natDegree_eq_one_of_irreducible

deleted theorem Polynomial.Splits.natDegree_le_one_of_irreducible

deleted theorem Polynomial.Splits.nextCoeff_eq_neg_sum_roots_mul_leadingCoeff

deleted theorem Polynomial.Splits.nextCoeff_eq_neg_sum_roots_of_monic

deleted theorem Polynomial.Splits.of_algHom

deleted theorem Polynomial.Splits.of_degree_eq_one

deleted theorem Polynomial.Splits.of_degree_eq_two

deleted theorem Polynomial.Splits.of_degree_le_one

deleted theorem Polynomial.Splits.of_dvd

deleted theorem Polynomial.Splits.of_isScalarTower

deleted theorem Polynomial.Splits.of_natDegree_eq_one

deleted theorem Polynomial.Splits.of_natDegree_eq_two

deleted theorem Polynomial.Splits.of_natDegree_le_one

deleted theorem Polynomial.Splits.of_splits_map

deleted theorem Polynomial.Splits.roots_ne_zero

deleted theorem Polynomial.Splits.splits

deleted theorem Polynomial.Splits.taylor

deleted def Polynomial.Splits

deleted theorem Polynomial.eval_rootOfSplits

deleted theorem Polynomial.map_sub_roots_sprod_eq_prod_map_eval

deleted theorem Polynomial.map_sub_sprod_roots_eq_prod_map_eval

deleted theorem Polynomial.splits_X_sub_C_mul_iff

deleted theorem Polynomial.splits_iff_card_roots

deleted theorem Polynomial.splits_iff_comp_splits_of_degree_eq_one

deleted theorem Polynomial.splits_iff_comp_splits_of_natDegree_eq_one

deleted theorem Polynomial.splits_iff_exists_multiset'

deleted theorem Polynomial.splits_iff_exists_multiset

deleted theorem Polynomial.splits_iff_splits

deleted theorem Polynomial.splits_mul_iff

deleted theorem Polynomial.splits_neg_iff

deleted theorem Polynomial.splits_of_degree_le_one_of_invertible

deleted theorem Polynomial.splits_of_degree_le_one_of_monic

deleted theorem Polynomial.splits_of_degree_le_zero

deleted theorem Polynomial.splits_of_natDegree_eq_zero

deleted theorem Polynomial.splits_of_natDegree_le_one_of_invertible

deleted theorem Polynomial.splits_of_natDegree_le_one_of_monic

deleted theorem Polynomial.splits_prod_iff

Modified Mathlib/Algebra/Polynomial/Splits.lean

added theorem IsUnit.splits

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.adjoin_rootSet_eq_range

added theorem Polynomial.Splits.aeval_eq_prod_aroots

added theorem Polynomial.Splits.aeval_eq_prod_aroots_of_monic

added theorem Polynomial.Splits.coeff_zero_eq_leadingCoeff_mul_prod_roots

added theorem Polynomial.Splits.coeff_zero_eq_prod_roots_of_monic

added theorem Polynomial.Splits.comp_X_add_C

added theorem Polynomial.Splits.comp_X_sub_C

added theorem Polynomial.Splits.comp_neg_X

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

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.dvd_iff_roots_le_roots

added theorem Polynomial.Splits.dvd_of_roots_le_roots

added theorem Polynomial.Splits.eq_X_sub_C_of_single_root

added theorem Polynomial.Splits.eq_prod_roots

added theorem Polynomial.Splits.eq_prod_roots_of_monic

added theorem Polynomial.Splits.eval_derivative

added theorem Polynomial.Splits.eval_derivative_div_eval_of_ne_zero

added theorem Polynomial.Splits.eval_derivative_eq_eval_mul_sum

added theorem Polynomial.Splits.eval_eq_prod_roots

added theorem Polynomial.Splits.eval_eq_prod_roots_of_monic

added theorem Polynomial.Splits.eval_root_derivative

added theorem Polynomial.Splits.exists_eval_eq_zero

added theorem Polynomial.Splits.image_rootSet

added theorem Polynomial.Splits.listProd

added theorem Polynomial.Splits.map_roots

added theorem Polynomial.Splits.mem_lift_of_roots_mem_range

added theorem Polynomial.Splits.mem_range_of_isRoot

added theorem Polynomial.Splits.mem_subfield_of_isRoot

added theorem Polynomial.Splits.monomial

added theorem Polynomial.Splits.multisetProd

added theorem Polynomial.Splits.natDegree_eq_card_roots

added theorem Polynomial.Splits.natDegree_eq_one_of_irreducible

added theorem Polynomial.Splits.natDegree_le_one_of_irreducible

added theorem Polynomial.Splits.nextCoeff_eq_neg_sum_roots_mul_leadingCoeff

added theorem Polynomial.Splits.nextCoeff_eq_neg_sum_roots_of_monic

added theorem Polynomial.Splits.of_algHom

added theorem Polynomial.Splits.of_degree_eq_one

added theorem Polynomial.Splits.of_degree_eq_two

added theorem Polynomial.Splits.of_degree_le_one

added theorem Polynomial.Splits.of_dvd

added theorem Polynomial.Splits.of_isScalarTower

added theorem Polynomial.Splits.of_natDegree_eq_one

added theorem Polynomial.Splits.of_natDegree_eq_two

added theorem Polynomial.Splits.of_natDegree_le_one

added theorem Polynomial.Splits.of_splits_map

added theorem Polynomial.Splits.roots_ne_zero

added theorem Polynomial.Splits.splits

added theorem Polynomial.Splits.taylor

added def Polynomial.Splits

added theorem Polynomial.eval_rootOfSplits

added theorem Polynomial.map_sub_roots_sprod_eq_prod_map_eval

added theorem Polynomial.map_sub_sprod_roots_eq_prod_map_eval

added theorem Polynomial.splits_X_sub_C_mul_iff

added theorem Polynomial.splits_iff_card_roots

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_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_one_of_invertible

added theorem Polynomial.splits_of_degree_le_one_of_monic

added theorem Polynomial.splits_of_degree_le_zero

added theorem Polynomial.splits_of_natDegree_eq_zero

added theorem Polynomial.splits_of_natDegree_le_one_of_invertible

added theorem Polynomial.splits_of_natDegree_le_one_of_monic

added theorem Polynomial.splits_prod_iff

Modified Mathlib/RingTheory/Polynomial/ScaleRoots.lean