Documentation

Mathlib.Algebra.Polynomial.UnitTrinomial

Unit Trinomials #

This file defines irreducible trinomials and proves an irreducibility criterion.

Main definitions #

Main results #

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

Shorthand for a trinomial

Equations
Instances For
    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}

    A unit trinomial is a trinomial with unit coefficients.

    Equations
    Instances For
      theorem Polynomial.IsUnitTrinomial.not_isUnit {p : Polynomial } (hp : p.IsUnitTrinomial) :
      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 kp.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) :
      theorem Polynomial.IsUnitTrinomial.irreducible_of_isCoprime {p : Polynomial } (hp : p.IsUnitTrinomial) (h : IsCoprime p p.mirror) :

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