Adjoining a primitive root of unity adjoins all of them

In a field extension K of F, the n-th roots of unity are exactly the powers of a primitive one, so adjoining a single primitive n-th root of unity to F already produces an intermediate field containing every n-th root of unity of K.

Main results

• IsPrimitiveRoot.mem_adjoin_of_pow_eq_one: an n-th root of unity lies in the intermediate field generated by a primitive n-th root of unity.

theorem IsPrimitiveRoot.mem_adjoin_of_pow_eq_one {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] {n : ℕ} [NeZero n] {ζ : K} (hζ : IsPrimitiveRoot ζ n) {μ : K} (hμ : μ ^ n = 1) : μ ∈ F⟮ζ⟯

Every n-th root of unity of a field extension K of F lies in the intermediate field generated over F by a primitive n-th root of unity, being one of its powers.