Commit 2025-10-30 10:23 0517a13f

View on Github →

refactor(FieldTheory/IsAlgClosed,IsSepClosed): redefine in terms of Polynomial.Factors (#30869) This PR redefines IsAlgClosed and IsSepClosed in terms of Polynomial.Factors rather than in terms of Polynomial.Splits (RingHom.id k). This is part of a larger effort to switch over from Polynomial.Splits to Polynomial.Factors.

Estimated changes

Modified Mathlib/FieldTheory/IsAlgClosed/Basic.lean

added theorem IsAlgClosed.splits

Modified Mathlib/FieldTheory/IsSepClosed.lean

added theorem IsSepClosed.splits_of_separable