# 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.

source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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 `p`th root in `K`. Then the polynomial `x ^ p - t` is irreducible over `K`.

source
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