Documentation

Mathlib.FieldTheory.KummerPolynomial

Irreducibility of X ^ p - a #

Main result #

theorem root_X_pow_sub_C_ne_zero' {K : Type u} [Field K] {n : Nat} {a : K} (hn : LT.lt 0 n) (ha : Ne a 0) :
theorem pow_ne_of_irreducible_X_pow_sub_C {K : Type u} [Field K] {n : Nat} {a : K} (H : Irreducible (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe Polynomial.C a))) {m : Nat} (hm : Dvd.dvd m n) (hm' : Ne m 1) (b : K) :
Ne (HPow.hPow b m) a
theorem X_pow_sub_C_irreducible_of_prime {K : Type u} [Field K] {p : Nat} (hp : Nat.Prime p) {a : K} (ha : ∀ (b : K), Ne (HPow.hPow b p) 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.

Stacks Tag 09HF (We proved the result without the condition that K is char p in 09HF.)