Kronecker-Weber, wild step for odd $p$: an abelian field of degree $p^k$ unramified outside $p$ lies in $\mathbb{Q}(\zeta_{p^N})$

Let $p$ be an odd prime and let $K$ be a finite abelian extension of $\mathbb{Q}$ of degree $p^k$. Assume that each prime $\ell \ne p$ is unramified in $K$. The statement asserts that there is $N \ge 0$ and an embedding of fields

Proof idea. The key fact is that for odd $p$ there is exactly one cyclic extension of $\mathbb{Q}$ of degree $p$ that is unramified outside $p$, namely the subfield of degree $p$ of $\mathbb{Q}(\zeta_{p^2})$. It follows that the Galois group of $K$ has at most one subgroup of index $p$, so it is cyclic. Let $K_m$ be the subfield of degree $p^m$ of $\mathbb{Q}(\zeta_{p^{m+1}})$ with $p^m = [K : \mathbb{Q}]$. The compositum $K K_m$ is abelian of $p$-power degree and unramified outside $p$, so its Galois group is cyclic by the same argument; it has the two quotients of order $p^m$ that correspond to $K$ and $K_m$, hence $K = K_m$.

Use. With the tame step (NumberField.exists_isUnramifiedIn_le_sup_of_prime_ne) this gives the Kronecker-Weber theorem for abelian fields of odd prime-power degree. This is a child of Leopoldt.exists_algHom_cyclotomicField_of_isCyclic_primePow.

Formalization Note. "Abelian" is IsAbelianGalois ℚ K; "$\ell$ unramified in $K$" is Algebra.IsUnramifiedIn (𝓞 K) (Ideal.span {(ℓ : ℤ)}); the conclusion is Nonempty (K →ₐ[ℚ] CyclotomicField (p ^ N) ℚ). For $k = 0$ take $N = 0$. The hypothesis $p \ne 2$ is necessary for the uniqueness argument: there are three quadratic fields unramified outside $2$. Mathlib has ZMod.isCyclic_units_of_prime_pow, IsCyclotomicExtension.Rat.galEquivZMod, Minkowski's theorem (NumberField.exists_not_isUnramifiedIn) and Kummer theory (Mathlib.FieldTheory.KummerExtension). The uniqueness of the cyclic degree $p$ field unramified outside $p$ is the hard part and is not in Mathlib.