Theorem Polynomial.IsSplittingField.splits

Modification history

2025-11-20 19:42

Mathlib/FieldTheory/SplittingField/IsSplittingField.lean

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

Modified Polynomial.IsSplittingField.splits View on Github →

2023-06-06 05:32

Mathlib/FieldTheory/SplittingField/IsSplittingField.lean

feat: port FieldTheory.SplittingField.IsSplittingField (#4714)

Added Polynomial.IsSplittingField.splits View on Github →