Cyclotomic fields lie in finite composita of prime-power towers

The field generated by the m-th roots of unity lies in the compositum of the prime-power cyclotomic towers for the primes dividing m. No primitive root or separability hypothesis is needed. This lets statements about finite composita of towers apply to a cyclotomic extension with arbitrary nonzero conductor.

References

• J. S. Milne, Class Field Theory, v4.03, Chapter VII, Lemma 8.4.

theorem IntermediateField.adjoin_nth_roots_le_iSup_adjoin_prime_pow {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {m : ℕ} (hm : m ≠ 0) : adjoin K {ζ : L | ζ ^ m = 1} ≤ ⨆ (q : ↥m.primeFactors), adjoin K {ζ : L | ∃ (r : ℕ), ζ ^ ↑q ^ r = 1}

The field generated by the m-th roots of unity lies in the compositum of the prime-power cyclotomic towers at the prime divisors of m.