Commit 2025-11-27 13:47 4e935591

feat(CyclotomicField): splitting of the prime p in ℚ⟮ζₘ⟯ when p does not divide m (#31946) This PR proves that when the prime p does not divide m, it splits completely in the cyclotomic field ℚ(ζₘ). Also change liesOver_span_zeta_sub_one from a theorem to an instance for better typeclass inference