Kronecker--Weber for cyclic extensions of prime-power degree

Kronecker–Weber theorem, cyclic prime-power case. Let $\mathbb{K}$ be a number field which is a Galois extension of $\mathbb{Q}$ whose Galois group $\mathrm{Gal}(\mathbb{K}/\mathbb{Q})$ is cyclic, and suppose $[\mathbb{K}:\mathbb{Q}] = p^k$ for a prime $p$ and some $k \ge 0$. Then there is an integer $n \ge 1$ and an embedding of $\mathbb{Q}$-algebras

This is the case to which the general Kronecker–Weber theorem is reduced in Washington's proof: a finite abelian group is a product of cyclic groups of prime-power order, so every abelian number field is the compositum of subfields with cyclic Galois group of prime-power order, and a compositum of subfields of cyclotomic fields lies in a cyclotomic field. The remaining (hard) work — reduction to extensions ramified only at $p$, and the analysis of those via ramification groups — is exactly the content of this statement. The cases $k \le 1$ with $p = 2$ (degree $\le 2$) are covered by NumberField.exists_algHom_cyclotomicField_of_finrank_le_two.

Formalization note. Galois is IsGalois ℚ K, cyclicity is IsCyclic (K ≃ₐ[ℚ] K), the degree hypothesis is Module.finrank ℚ K = p ^ k with p.Prime, $\mathbb{Q}(\zeta_n)$ is CyclotomicField n ℚ, and the embedding is an unspecified K →ₐ[ℚ] CyclotomicField n ℚ.