$\mathbb{Q}(\zeta_m)$ embeds in $\mathbb{Q}(\zeta_k)$ when $m \mid k$

Let $m, k \ge 1$ be integers with $m \mid k$. Then there is an embedding of $\mathbb{Q}$-algebras

Indeed, if $\zeta$ is a primitive $k$-th root of unity in $\mathbb{Q}(\zeta_k)$, then $\zeta^{k/m}$ is a primitive $m$-th root of unity, so the $m$-th cyclotomic polynomial splits in $\mathbb{Q}(\zeta_k)$, and $\mathbb{Q}(\zeta_m)$, being its splitting field, embeds.

Formalization note. $\mathbb{Q}(\zeta_n)$ is Mathlib's CyclotomicField n ℚ (the splitting field of the $n$-th cyclotomic polynomial over $\mathbb{Q}$).