Theorems · Theorem · field theory

Algebra.adjoin_root_eq_top_of_isSplittingField

∀ {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)] {α : L},
          α ^ n = (algebraMap K L) a → K[α] = ⊤

Defined in

Mathlib.FieldTheory.KummerExtension

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraPolynomial.IsSplittingField