Commit 2025-12-08 06:22 7b56cbf1

View on Github →

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

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

added theorem Polynomial.Splits.eval_eq_prod_roots

added theorem Polynomial.Splits.eval_eq_prod_roots_of_monic

added theorem Polynomial.Splits.mem_range_of_isRoot

added theorem Polynomial.Splits.mem_subfield_of_isRoot

Modified Mathlib/Algebra/Polynomial/Splits.lean

deleted theorem Polynomial.Splits.mem_subfield_of_isRoot

deleted theorem Polynomial.adjoin_rootSet_eq_range

deleted theorem Polynomial.aeval_eq_prod_aroots_sub_of_monic_of_splits

deleted theorem Polynomial.aeval_eq_prod_aroots_sub_of_splits

deleted theorem Polynomial.aeval_root_of_mapAlg_eq_multiset_prod_X_sub_C

deleted theorem Polynomial.eq_X_sub_C_of_splits_of_single_root

deleted theorem Polynomial.eval_eq_prod_roots_sub_of_monic_of_splits_id

deleted theorem Polynomial.eval_eq_prod_roots_sub_of_splits_id

Modified Mathlib/FieldTheory/KummerExtension.lean

Modified Mathlib/FieldTheory/Separable.lean

Modified Mathlib/FieldTheory/SplittingField/IsSplittingField.lean

Modified Mathlib/RingTheory/Polynomial/Tower.lean

added theorem Polynomial.aeval_root_of_mapAlg_eq_multiset_prod_X_sub_C