Theorems · Definition · field theory

autEquivRootsOfUnity

{K : Type u} →
  [inst : Field K] →
    {n : ℕ} →
      (primitiveRoots n K).Nonempty →
        {a : K} →
          Irreducible (Polynomial.X ^ n - Polynomial.C a) →
            (L : Type u_1) →
              [inst_1 : Field L] →
                [inst_2 : Algebra K L] →
                  [Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)] →
                    [NeZero n] → Gal(L/K) ≃* ↥(rootsOfUnity n K)

Suppose L/K is the splitting field of Xⁿ - a, then Gal(L/K) is isomorphic to the roots of unity in K if K contains all of them. Note that this does not depend on a choice of ⁿ√a.

Defined in

Mathlib.FieldTheory.KummerExtension

Cited by

4 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraPolynomial.IsSplittingFieldNeZero