Theorems · Theorem · field theory

X_pow_sub_C_irreducible_of_prime

∀ {K : Type u} [inst : Field K] {p : ℕ},
  Nat.Prime p → ∀ {a : K}, (∀ (b : K), b ^ p ≠ a) → Irreducible (Polynomial.X ^ p - Polynomial.C a)

Let p be a prime number. Let K be a field. Let t ∈ K be an element which does not have a pth root in K. Then the polynomial x ^ p - t is irreducible over K.

Defined in

Mathlib.FieldTheory.KummerPolynomial

Cited by

2 results in Mathlib

Foundations

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

Assumes

Field