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.coeff (Polynomial.trinomial k m n u v w) 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.coeff (Polynomial.trinomial k m n u v w) 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.coeff (Polynomial.trinomial k m n u v w) 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.natDegree (Polynomial.trinomial k m n u v w) = 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.natTrailingDegree (Polynomial.trinomial k m n u v w) = 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.leadingCoeff (Polynomial.trinomial k m n u v w) = 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.trailingCoeff (Polynomial.trinomial k m n u v w) = 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.Monic (Polynomial.trinomial k m n u v 1)

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.mirror (Polynomial.trinomial k m n u v w) = 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.support (Polynomial.trinomial k m n u v w) = {k, m, n}

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

A unit trinomial is a trinomial with unit coefficients.

Equations

• Polynomial.IsUnitTrinomial p = ∃ (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 : Polynomial.IsUnitTrinomial p) : ¬IsUnit p

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

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

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

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

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

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

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

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

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 * Polynomial.mirror p).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 * Polynomial.mirror p = q * Polynomial.mirror q) : q = p ∨ q = Polynomial.mirror p

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 * Polynomial.mirror p = q * Polynomial.mirror q) : q = p ∨ q = Polynomial.mirror p

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

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

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

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

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