Theorem Polynomial.splits_id_of_splits

Modification history

2025-11-20 19:42
Mathlib/Algebra/Polynomial/Splits.lean
feat(Algebra/Polynomial/Splits): remove the `RingHom` argument of `Splits` (#31631)
Modified Polynomial.splits_id_of_splitsView on Github →
2023-11-01 13:33
Mathlib/Data/Polynomial/Splits.lean
refactor: golf Normal.of_isSplittingField (#8004) …
Added Polynomial.splits_id_of_splitsView on Github →