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 v w : R) : Polynomial R

Shorthand for a trinomial

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

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

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

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

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

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

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

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

theorem Polynomial.trinomial_support {R : Type u_1} [Semiring R] {k m n : ℕ} {u v w : R} (hkm : k < m) (hmn : m < n) (hu : u ≠ 0) (hv : v ≠ 0) (hw : w ≠ 0) : (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.

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 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 = trinomial k m n ↑u ↑v ↑w) : C ↑v * (C ↑u * X ^ (m + n) + C ↑w * 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 q : Polynomial ℤ} {k m m' n : ℕ} (hkm : k < m) (hmn : m < n) (hkm' : k < m') (hmn' : m' < n) (u v w : ℤˣ) (hp : p = trinomial k m n ↑u ↑v ↑w) (hq : q = 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 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 = trinomial k m n ↑u ↑v ↑w) (hq : q = 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