Theorems · Definition · field theory

autAdjoinRootXPowSubCEquiv

{K : Type u} →
  [inst : Field K] →
    {n : ℕ} →
      (primitiveRoots n K).Nonempty →
        {a : K} →
          Irreducible (Polynomial.X ^ n - Polynomial.C a) →
            [NeZero n] →
              ↥(rootsOfUnity n K) ≃*
                AdjoinRoot (Polynomial.X ^ n - Polynomial.C a) ≃ₐ[K] AdjoinRoot (Polynomial.X ^ n - Polynomial.C a)

The equivalence between the roots of unity of K and Gal(K[ⁿ√a]/K).

Defined in

Mathlib.FieldTheory.KummerExtension

Cited by

4 results in Mathlib

Foundations

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

Assumes

FieldNeZero