Commit 2025-12-09 05:22 996ee984

View on Github →

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

added theorem Polynomial.Splits.eval_root_derivative

added theorem Polynomial.Splits.of_splits_map

Modified Mathlib/Algebra/Polynomial/Splits.lean

deleted theorem Polynomial.aeval_derivative_of_splits

deleted theorem Polynomial.aeval_root_derivative_of_splits

deleted theorem Polynomial.eval_derivative_of_splits

deleted theorem Polynomial.eval₂_derivative_of_splits

deleted theorem Polynomial.splits_comp_of_splits

deleted theorem Polynomial.splits_id_of_splits

deleted theorem Polynomial.splits_of_comp

Modified Mathlib/FieldTheory/Galois/Basic.lean

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

Modified Mathlib/FieldTheory/Normal/Basic.lean

Modified Mathlib/FieldTheory/Normal/Defs.lean

Modified Mathlib/FieldTheory/PolynomialGaloisGroup.lean

Modified Mathlib/FieldTheory/SplittingField/IsSplittingField.lean

Modified Mathlib/RingTheory/Discriminant.lean