Theorem Polynomial.cyclotomic'_splits

Modification history

2025-11-23 19:05
Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
refactor: clean up occurrences of `Splits (p.map (RingHom.id _))` (#31915) …
Modified Polynomial.cyclotomic'_splitsView on Github →
2025-11-20 19:42
Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
feat(Algebra/Polynomial/Splits): remove the `RingHom` argument of `Splits` (#31631)
Modified Polynomial.cyclotomic'_splitsView on Github →
2023-06-07 15:05
Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
feat: port RingTheory.Polynomial.Cyclotomic.Basic (#4805)
Added Polynomial.cyclotomic'_splitsView on Github →