English
If L/K is S-cyclotomic and M is a sep-closed field, there exists a K-algebra isomorphism from L to the adjoin of the S-th roots of unity in M.
Русский
Если L/K циклотомическое по S и M — сепарированное поле, существует K-алгебраическое изоморфизм L к adjoin K корням единицы степеней из S в M.
LaTeX
$$$\\exists \\varphi: L \\cong_K \\operatorname{adjoin}_K\\{ x \\in M \\mid \\exists n \\in S, n \\neq 0 \\land x^n = 1 \\}$$$
Lean4
/-- Any two `S`-cyclotomic extensions are isomorphic. -/
noncomputable def algEquiv [IsCyclotomicExtension S K L] (L' : Type*) [Field L'] [Algebra K L']
[IsCyclotomicExtension S K L'] : L ≃ₐ[K] L' :=
(nonempty_algEquiv_adjoin_of_isSepClosed S K L (AlgebraicClosure K)).some.trans
(nonempty_algEquiv_adjoin_of_isSepClosed S K L' (AlgebraicClosure K)).some.symm
