Theorem Polynomial.exists_finset_of_splits

Modification history

2025-11-20 19:42

Mathlib/FieldTheory/Separable.lean

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

Modified Polynomial.exists_finset_of_splits View on Github →

2023-05-23 16:17

Mathlib/FieldTheory/Separable.lean

feat: port FieldTheory.Separable (#4272)

Added Polynomial.exists_finset_of_splits View on Github →