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 : ℕ) (a : K) : AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a) ^ n = (AdjoinRoot.of (Polynomial.X ^ n - Polynomial.C a)) a

theorem root_X_pow_sub_C_ne_zero {K : Type u} [Field K] {n : ℕ} (hn : 1 < n) (a : K) : AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a) ≠ 0

theorem root_X_pow_sub_C_ne_zero' {K : Type u} [Field K] {n : ℕ} {a : K} (hn : 0 < n) (ha : a ≠ 0) : AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a) ≠ 0

theorem ne_zero_of_irreducible_X_pow_sub_C {K : Type u} [Field K] {n : ℕ} {a : K} (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) : n ≠ 0

theorem ne_zero_of_irreducible_X_pow_sub_C' {K : Type u} [Field K] {n : ℕ} (hn : n ≠ 1) {a : K} (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) : a ≠ 0

theorem root_X_pow_sub_C_eq_zero_iff {K : Type u} [Field K] {n : ℕ} {a : K} (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) : AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a) = 0 ↔ a = 0

theorem root_X_pow_sub_C_ne_zero_iff {K : Type u} [Field K] {n : ℕ} {a : K} (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) : AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a) ≠ 0 ↔ a ≠ 0

theorem pow_ne_of_irreducible_X_pow_sub_C {K : Type u} [Field K] {n : ℕ} {a : K} (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) {m : ℕ} (hm : m ∣ n) (hm' : m ≠ 1) (b : K) : b ^ m ≠ a

theorem X_pow_sub_C_irreducible_of_prime {K : Type u} [Field K] {p : ℕ} (hp : Nat.Prime p) {a : K} (ha : ∀ (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.

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 : ℕ} (hp : Nat.Prime p) {a : K} : Irreducible (Polynomial.X ^ p - Polynomial.C a) ↔ ∀ (b : K), b ^ p ≠ a