Theorem IsAlgClosed.splits

Modification history

2025-11-20 19:42

Mathlib/FieldTheory/IsAlgClosed/Basic.lean

feat(Algebra/Polynomial/Splits): remove the `RingHom` argument of `Splits` (#31631)

Modified IsAlgClosed.splits View 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.splits View on Github →