Theorems · Theorem · field theory

exists_root_adjoin_eq_top_of_isCyclic

∀ (K : Type u) [inst : Field K] (L : Type u_1) [inst_1 : Field L] [inst_2 : Algebra K L] [FiniteDimensional K L],
  (primitiveRoots (Module.finrank K L) K).Nonempty →
    ∀ [IsGalois K L] [IsCyclic Gal(L/K)], ∃ α, α ^ Module.finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤

If L/K is a cyclic extension of degree n, and K contains all n-th roots of unity, then L = K[α] for some α ^ n ∈ K.

Defined in

Mathlib.FieldTheory.KummerExtension

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraFiniteDimensionalIsGaloisIsCyclic