Irreducibility of X ^ p - a

Main result

• X_pow_sub_C_irreducible_iff_of_prime: For p prime, X ^ p - C a is irreducible iff a is not a p-power. This is not true for composite n. For example, x^4+4=(x^2-2x+2)(x^2+2x+2) but -4 is not a 4th power.

theorem root_X_pow_sub_C_pow {K : Type u} [Field K] (n : Nat) (a : K) : Eq (HPow.hPow (AdjoinRoot.root (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe Polynomial.C a))) n) (DFunLike.coe (AdjoinRoot.of (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe Polynomial.C a))) a)

theorem root_X_pow_sub_C_ne_zero {K : Type u} [Field K] {n : Nat} (hn : LT.lt 1 n) (a : K) : Ne (AdjoinRoot.root (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe Polynomial.C a))) 0

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) : Ne (AdjoinRoot.root (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe Polynomial.C a))) 0

theorem ne_zero_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))) : Ne n 0

theorem ne_zero_of_irreducible_X_pow_sub_C' {K : Type u} [Field K] {n : Nat} (hn : Ne n 1) {a : K} (H : Irreducible (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe Polynomial.C a))) : Ne a 0

theorem root_X_pow_sub_C_eq_zero_iff {K : Type u} [Field K] {n : Nat} {a : K} (H : Irreducible (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe Polynomial.C a))) : Iff (Eq (AdjoinRoot.root (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe Polynomial.C a))) 0) (Eq a 0)

theorem root_X_pow_sub_C_ne_zero_iff {K : Type u} [Field K] {n : Nat} {a : K} (H : Irreducible (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe Polynomial.C a))) : Iff (Ne (AdjoinRoot.root (HSub.hSub (HPow.hPow Polynomial.X n) (DFunLike.coe Polynomial.C a))) 0) (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) : Irreducible (HSub.hSub (HPow.hPow Polynomial.X p) (DFunLike.coe 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.

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

theorem X_pow_sub_C_irreducible_iff_of_prime {K : Type u} [Field K] {p : Nat} (hp : Nat.Prime p) {a : K} : Iff (Irreducible (HSub.hSub (HPow.hPow Polynomial.X p) (DFunLike.coe Polynomial.C a))) (∀ (b : K), Ne (HPow.hPow b p) a)