I have a question about a step in a proof from Lang's "Algebra": Thm. 7.2 (page 292). Here the excerpt & tagged problem:
During the proof the author defines $F:= k(\zeta)$ where $\zeta$ is the primitive $m$-root. Obviously $F/k$ is clearly abelian since $Gal(F,k)=(\mathbb{Z}/m)^*$.
My question is why does it imply that then the compositum $KF$ is solvable over $F$? (definition: https://en.wikipedia.org/wiki/Solvable_group)
By assumption $K$ was finite solvable over $k$. Is there a way to derive solvability of $KF$ over $F$ from this?
Since $K/k$ is finite Galois, $KF/F$ is finite Galois.
Also, $\text{Gal}(KF/F)$ is embedded in $\text{Gal}(K/k)$, where the embedding is restricting automorphisms in $\text{Gal}(KF/K)$ to $E$.
Since $\text{Gal}(K/k)$ is solvable, so is $\text{Gal}(KF/K)$. That is, $KF/K$ is solvable.