Theorem IsSepClosed.splits_of_separable

Modification history

2025-11-28 14:12
Mathlib/FieldTheory/IsSepClosed.lean
refactor(FieldTheory/IsAlgClosed,IsSepClosed): rename from `factors` to `splits` (#32036) …
Deleted IsSepClosed.splits_of_separableView on Github →
2025-10-30 10:23
Mathlib/FieldTheory/IsSepClosed.lean
refactor(FieldTheory/IsAlgClosed,IsSepClosed): redefine in terms of `Polynomial.Factors` (#30869) …
Added IsSepClosed.splits_of_separableView on Github →