Theorem IsAlgClosed.splits

Modification history

2025-11-28 14:12
Mathlib/FieldTheory/IsAlgClosed/Basic.lean
refactor(FieldTheory/IsAlgClosed,IsSepClosed): rename from `factors` to `splits` (#32036) …
Deleted IsAlgClosed.splitsView on Github →
2025-11-23 19:05
Mathlib/FieldTheory/IsAlgClosed/Basic.lean
refactor: clean up occurrences of `Splits (p.map (RingHom.id _))` (#31915) …
Modified IsAlgClosed.splitsView on Github →
2025-11-20 19:42
Mathlib/FieldTheory/IsAlgClosed/Basic.lean
feat(Algebra/Polynomial/Splits): remove the `RingHom` argument of `Splits` (#31631)
Modified IsAlgClosed.splitsView on Github →
2025-10-30 10:23
Mathlib/FieldTheory/IsAlgClosed/Basic.lean
refactor(FieldTheory/IsAlgClosed,IsSepClosed): redefine in terms of `Polynomial.Factors` (#30869) …
Added IsAlgClosed.splitsView on Github →