English
If for every n ∈ S with n ≠ 0 there exists r ∈ M that is a primitive root of unity of order n, then there exists a K-algebra isomorphism from L to the adjoin of { x ∈ M | ∃ n ∈ S, n ≠ 0 ∧ x^n = 1 }.
Русский
Если для каждого n ∈ S, n ≠ 0 найдется r ∈ M, который является примитивным корнем единицы порядка n, то существует K-алгебраический изоморфизм L к adjoin_K { x ∈ M | ∃ n ∈ S, n ≠ 0 ∧ x^n = 1 }.
LaTeX
$$$(\\forall n \\in S, n \\neq 0 \\Rightarrow \\exists r \\in M, IsPrimitiveRoot(r,n)) \\Rightarrow \\exists \\varphi: L \\cong_K \\operatorname{adjoin}_K\\{ x \\in M \\mid \\exists n \\in S, n \\neq 0 \\land x^n = 1 \\}$$$
Lean4
theorem nonempty_algEquiv_adjoin_of_exists_isPrimitiveRoot [IsCyclotomicExtension S K L] (M : Type*) [Field M]
[Algebra K M] (h : ∀ n ∈ S, n ≠ 0 → ∃ r : M, IsPrimitiveRoot r n) :
Nonempty (L ≃ₐ[K] IntermediateField.adjoin K {x : M | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) :=
have := IntermediateField.isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot S K M h
⟨algEquiv S K L _⟩
