Theorems · Theorem · field theory

isCyclic_tfae

∀ (K : Type u_1) (L : Type u_2) [inst : Field K] [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),
        ∃ a,
          Irreducible (Polynomial.X ^ Module.finrank K L - Polynomial.C a) ∧
            Polynomial.IsSplittingField K L (Polynomial.X ^ Module.finrank K L - Polynomial.C a),
        ∃ α, α ^ Module.finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤].TFAE

Suppose L/K is a finite extension of dimension n, and K contains a primitiven-th root of unity. Then L/K is cyclic iff L is a splitting field of some irreducible polynomial of the form Xⁿ - a : K[X] iff L = K[α] for some αⁿ ∈ K.

Defined in

Mathlib.FieldTheory.KummerExtension

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraFiniteDimensional