∀ {n : ℕ} [NeZero n] {S : Set ℕ} (K : Type w) (L : Type z) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [H : IsCyclotomicExtension S K L], n ∈ S → (Polynomial.map (algebraMap K L) (Polynomial.X ^ n - 1)).Splits