Theorem NumberField.RingOfIntegers.minpoly_coe

feat(CyclotomicField): splitting of the prime `p` in `ℚ⟮ζₘ⟯` when `p` does not divide `m` (#31946) …