Theorems · Definition · field theory

autEquivZmod

{K : Type u} →
  [inst : Field K] →
    {n : ℕ} →
      {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] → {ζ : K} → IsPrimitiveRoot ζ n → Gal(L/K) ≃* Multiplicative (ZMod n)

Suppose L/K is the splitting field of Xⁿ - a, and ζ is an n-th primitive root of unity in K, then Gal(L/K) is isomorphic to ZMod n.

Defined in

Mathlib.FieldTheory.KummerExtension

Cited by

5 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraPolynomial.IsSplittingFieldNeZero