Commit 2025-12-15 11:03 1f81f0f0

View on Github →

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

added theorem Polynomial.Splits.of_algHom

added theorem Polynomial.Splits.of_degree_eq_two

added theorem Polynomial.Splits.of_isScalarTower

added theorem Polynomial.Splits.of_natDegree_eq_two

Modified Mathlib/Algebra/Polynomial/Splits.lean

deleted theorem Polynomial.mem_lift_of_splits_of_roots_mem_range

deleted theorem Polynomial.splits_of_algHom

deleted theorem Polynomial.splits_of_degree_eq_two

deleted theorem Polynomial.splits_of_isScalarTower

deleted theorem Polynomial.splits_of_natDegree_eq_two

Modified Mathlib/FieldTheory/Galois/Basic.lean

Modified Mathlib/FieldTheory/IsAlgClosed/Basic.lean

Modified Mathlib/FieldTheory/Isaacs.lean

Modified Mathlib/FieldTheory/Normal/Basic.lean

Modified Mathlib/RingTheory/Polynomial/GaussLemma.lean