Theorems · Theorem · number theory

IsCyclotomicExtension.nonempty_algEquiv_adjoin_of_isSepClosed

∀ (S : Set ℕ) (K : Type w) (L : Type z) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [IsCyclotomicExtension S K L] (M : Type u_1) [inst_4 : Field M] [inst_5 : Algebra K M] [IsSepClosed M],
  Nonempty (L ≃ₐ[K] ↥(IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}))

Defined in

Mathlib.NumberTheory.Cyclotomic.Basic

Cited by

1 results in Mathlib

Foundations

Depth 197 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldFieldAlgebraIsCyclotomicExtensionFieldAlgebraIsSepClosed