Theorems · Definition · field theory

adjoinRootXPowSubCEquiv

{K : Type u} →
  [inst : Field K] →
    {n : ℕ} →
      {a : K} →
        {L : Type u_1} →
          [inst_1 : Field L] →
            [inst_2 : Algebra K L] →
              [Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)] →
                {α : L} →
                  (primitiveRoots n K).Nonempty →
                    Irreducible (Polynomial.X ^ n - Polynomial.C a) →
                      α ^ n = (algebraMap K L) a → AdjoinRoot (Polynomial.X ^ n - Polynomial.C a) ≃ₐ[K] L

Suppose L/K is the splitting field of Xⁿ - a, then a choice of ⁿ√a gives an equivalence of L with K[n√a].

Defined in

Mathlib.FieldTheory.KummerExtension

Cited by

5 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraPolynomial.IsSplittingField