Primitive roots of unity in separably closed fields

Mathlib's IsSepClosed.hasEnoughRootsOfUnity provides primitive n-th roots of unity in a separably closed field E in which n is nonzero. Whether n is nonzero only depends on the characteristic, which is shared by all nontrivial algebras over a field K. Hence E contains a primitive n-th root of unity as soon as some domain over K does. For instance, the separable closure of K contains every primitive root of unity found in an algebraic closure of K.

Main results

• IsPrimitiveRoot.exists_isPrimitiveRoot_of_isSepClosed: a separably closed field over K contains a primitive n-th root of unity as soon as some domain over K does.

theorem IsPrimitiveRoot.exists_isPrimitiveRoot_of_isSepClosed (K : Type u_1) {E : Type u_2} {M : Type u_3} [Field K] [Field E] [IsSepClosed E] [Algebra K E] [CommRing M] [IsDomain M] [Algebra K M] {n : ℕ} {ζ : M} (hζ : IsPrimitiveRoot ζ n) : ∃ (ξ : E), IsPrimitiveRoot ξ n

A separably closed field E over a field K contains a primitive n-th root of unity as soon as some domain M over K does.