Irreducibility of X ^ p - a #
Main result #
X_pow_sub_C_irreducible_iff_of_prime: Forpprime,X ^ p - C ais irreducible iffais not ap-power. This is not true for compositen. For example,x^4+4=(x^2-2x+2)(x^2+2x+2)but-4is 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
ne_zero_of_irreducible_X_pow_sub_C
{K : Type u}
[Field K]
{n : ℕ}
{a : K}
(H : Irreducible (Polynomial.X ^ n - Polynomial.C a))
:
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))
:
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))
:
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))
:
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)
:
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.
theorem
X_pow_sub_C_irreducible_iff_of_prime
{K : Type u}
[Field K]
{p : ℕ}
(hp : Nat.Prime p)
{a : K}
: