Unit Trinomials

This file defines irreducible trinomials and proves an irreducibility criterion.

Main definitions

• Polynomial.IsUnitTrinomial

Main results

• Polynomial.IsUnitTrinomial.irreducible_of_coprime: An irreducibility criterion for unit trinomials.

noncomputable def Polynomial.trinomial {R : Type u_1} [Semiring R] (k : ℕ) (m : ℕ) (n : ℕ) (u : R) (v : R) (w : R) : Polynomial R

Shorthand for a trinomial

Equations

• Polynomial.trinomial k m n u v w = Polynomial.C u * Polynomial.X ^ k + Polynomial.C v * Polynomial.X ^ m + Polynomial.C w * Polynomial.X ^ n

theorem Polynomial.trinomial_def {R : Type u_1} [Semiring R] (k : ℕ) (m : ℕ) (n : ℕ) (u : R) (v : R) (w : R) : Polynomial.trinomial k m n u v w = Polynomial.C u * Polynomial.X ^ k + Polynomial.C v * Polynomial.X ^ m + Polynomial.C w * Polynomial.X ^ n

theorem Polynomial.trinomial_leading_coeff' {R : Type u_1} [Semiring R] {k : ℕ} {m : ℕ} {n : ℕ} {u : R} {v : R} {w : R} (hkm : k < m) (hmn : m < n) : (Polynomial.trinomial k m n u v w).coeff n = w

theorem Polynomial.trinomial_middle_coeff {R : Type u_1} [Semiring R] {k : ℕ} {m : ℕ} {n : ℕ} {u : R} {v : R} {w : R} (hkm : k < m) (hmn : m < n) : (Polynomial.trinomial k m n u v w).coeff m = v

theorem Polynomial.trinomial_trailing_coeff' {R : Type u_1} [Semiring R] {k : ℕ} {m : ℕ} {n : ℕ} {u : R} {v : R} {w : R} (hkm : k < m) (hmn : m < n) : (Polynomial.trinomial k m n u v w).coeff k = u

theorem Polynomial.trinomial_natDegree {R : Type u_1} [Semiring R] {k : ℕ} {m : ℕ} {n : ℕ} {u : R} {v : R} {w : R} (hkm : k < m) (hmn : m < n) (hw : w ≠ 0) : (Polynomial.trinomial k m n u v w).natDegree = n

theorem Polynomial.trinomial_natTrailingDegree {R : Type u_1} [Semiring R] {k : ℕ} {m : ℕ} {n : ℕ} {u : R} {v : R} {w : R} (hkm : k < m) (hmn : m < n) (hu : u ≠ 0) : (Polynomial.trinomial k m n u v w).natTrailingDegree = k

theorem Polynomial.trinomial_leadingCoeff {R : Type u_1} [Semiring R] {k : ℕ} {m : ℕ} {n : ℕ} {u : R} {v : R} {w : R} (hkm : k < m) (hmn : m < n) (hw : w ≠ 0) : (Polynomial.trinomial k m n u v w).leadingCoeff = w

theorem Polynomial.trinomial_trailingCoeff {R : Type u_1} [Semiring R] {k : ℕ} {m : ℕ} {n : ℕ} {u : R} {v : R} {w : R} (hkm : k < m) (hmn : m < n) (hu : u ≠ 0) : (Polynomial.trinomial k m n u v w).trailingCoeff = u

theorem Polynomial.trinomial_monic {R : Type u_1} [Semiring R] {k : ℕ} {m : ℕ} {n : ℕ} {u : R} {v : R} (hkm : k < m) (hmn : m < n) : (Polynomial.trinomial k m n u v 1).Monic

theorem Polynomial.trinomial_mirror {R : Type u_1} [Semiring R] {k : ℕ} {m : ℕ} {n : ℕ} {u : R} {v : R} {w : R} (hkm : k < m) (hmn : m < n) (hu : u ≠ 0) (hw : w ≠ 0) : (Polynomial.trinomial k m n u v w).mirror = Polynomial.trinomial k (n - m + k) n w v u

theorem Polynomial.trinomial_support {R : Type u_1} [Semiring R] {k : ℕ} {m : ℕ} {n : ℕ} {u : R} {v : R} {w : R} (hkm : k < m) (hmn : m < n) (hu : u ≠ 0) (hv : v ≠ 0) (hw : w ≠ 0) : (Polynomial.trinomial k m n u v w).support = {k, m, n}

def Polynomial.IsUnitTrinomial (p : Polynomial ℤ) : Prop

A unit trinomial is a trinomial with unit coefficients.

Equations

• p.IsUnitTrinomial = ∃ (k : ℕ) (m : ℕ) (n : ℕ) (_ : k < m) (_ : m < n) (u : ℤˣ) (v : ℤˣ) (w : ℤˣ), p = Polynomial.trinomial k m n ↑u ↑v ↑w

theorem Polynomial.IsUnitTrinomial.not_isUnit {p : Polynomial ℤ} (hp : p.IsUnitTrinomial) : ¬IsUnit p

theorem Polynomial.IsUnitTrinomial.card_support_eq_three {p : Polynomial ℤ} (hp : p.IsUnitTrinomial) : p.support.card = 3

theorem Polynomial.IsUnitTrinomial.ne_zero {p : Polynomial ℤ} (hp : p.IsUnitTrinomial) : p ≠ 0

theorem Polynomial.IsUnitTrinomial.coeff_isUnit {p : Polynomial ℤ} (hp : p.IsUnitTrinomial) {k : ℕ} (hk : k ∈ p.support) : IsUnit (p.coeff k)

theorem Polynomial.IsUnitTrinomial.leadingCoeff_isUnit {p : Polynomial ℤ} (hp : p.IsUnitTrinomial) : IsUnit p.leadingCoeff

theorem Polynomial.IsUnitTrinomial.trailingCoeff_isUnit {p : Polynomial ℤ} (hp : p.IsUnitTrinomial) : IsUnit p.trailingCoeff

theorem Polynomial.isUnitTrinomial_iff {p : Polynomial ℤ} : p.IsUnitTrinomial ↔ p.support.card = 3 ∧ ∀ k ∈ p.support, IsUnit (p.coeff k)

theorem Polynomial.isUnitTrinomial_iff' {p : Polynomial ℤ} : p.IsUnitTrinomial ↔ (p * p.mirror).coeff (((p * p.mirror).natDegree + (p * p.mirror).natTrailingDegree) / 2) = 3

theorem Polynomial.isUnitTrinomial_iff'' {p : Polynomial ℤ} {q : Polynomial ℤ} (h : p * p.mirror = q * q.mirror) : p.IsUnitTrinomial ↔ q.IsUnitTrinomial

theorem Polynomial.IsUnitTrinomial.irreducible_aux1 {p : Polynomial ℤ} {k : ℕ} {m : ℕ} {n : ℕ} (hkm : k < m) (hmn : m < n) (u : ℤˣ) (v : ℤˣ) (w : ℤˣ) (hp : p = Polynomial.trinomial k m n ↑u ↑v ↑w) : Polynomial.C ↑v * (Polynomial.C ↑u * Polynomial.X ^ (m + n) + Polynomial.C ↑w * Polynomial.X ^ (n - m + k + n)) = { toFinsupp := Finsupp.filter (fun (x : ℕ) => x ∈ Set.Ioo (k + n) (n + n)) (p * p.mirror).toFinsupp }

theorem Polynomial.IsUnitTrinomial.irreducible_aux2 {p : Polynomial ℤ} {q : Polynomial ℤ} {k : ℕ} {m : ℕ} {m' : ℕ} {n : ℕ} (hkm : k < m) (hmn : m < n) (hkm' : k < m') (hmn' : m' < n) (u : ℤˣ) (v : ℤˣ) (w : ℤˣ) (hp : p = Polynomial.trinomial k m n ↑u ↑v ↑w) (hq : q = Polynomial.trinomial k m' n ↑u ↑v ↑w) (h : p * p.mirror = q * q.mirror) : q = p ∨ q = p.mirror

theorem Polynomial.IsUnitTrinomial.irreducible_aux3 {p : Polynomial ℤ} {q : Polynomial ℤ} {k : ℕ} {m : ℕ} {m' : ℕ} {n : ℕ} (hkm : k < m) (hmn : m < n) (hkm' : k < m') (hmn' : m' < n) (u : ℤˣ) (v : ℤˣ) (w : ℤˣ) (x : ℤˣ) (z : ℤˣ) (hp : p = Polynomial.trinomial k m n ↑u ↑v ↑w) (hq : q = Polynomial.trinomial k m' n ↑x ↑v ↑z) (h : p * p.mirror = q * q.mirror) : q = p ∨ q = p.mirror

theorem Polynomial.IsUnitTrinomial.irreducible_of_coprime {p : Polynomial ℤ} (hp : p.IsUnitTrinomial) (h : IsRelPrime p p.mirror) : Irreducible p

theorem Polynomial.IsUnitTrinomial.irreducible_of_isCoprime {p : Polynomial ℤ} (hp : p.IsUnitTrinomial) (h : IsCoprime p p.mirror) : Irreducible p

A unit trinomial is irreducible if it is coprime with its mirror

theorem Polynomial.IsUnitTrinomial.irreducible_of_coprime' {p : Polynomial ℤ} (hp : p.IsUnitTrinomial) (h : ∀ (z : ℂ), ¬((Polynomial.aeval z) p = 0 ∧ (Polynomial.aeval z) p.mirror = 0)) : Irreducible p

A unit trinomial is irreducible if it has no complex roots in common with its mirror