Theorem Splits.algebraicClosure

Modification history

2025-11-20 19:42

Mathlib/FieldTheory/AlgebraicClosure.lean

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

Modified Splits.algebraicClosure View on Github →

2024-11-05 19:57

Mathlib/FieldTheory/AlgebraicClosure.lean

feat(FieldTheory/AlgebraicClosure): A polynomial splits in `E` implies it splits in `algebraicClosure F E` (#18331) …

Added Splits.algebraicClosure View on Github →