# mathlib3documentation

data.polynomial.unit_trinomial

# Unit Trinomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines irreducible trinomials and proves an irreducibility criterion.

## Main definitions #

• polynomial.is_unit_trinomial

## Main results #

• polynomial.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) :

Shorthand for a trinomial

Equations
• n u v w = + +
theorem polynomial.trinomial_def {R : Type u_1} [semiring R] (k m n : ) (u v w : R) :
n u v w = + +
theorem polynomial.trinomial_leading_coeff' {R : Type u_1} [semiring R] {k m n : } {u v w : R} (hkm : k < m) (hmn : m < n) :
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) :
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) :
n u v w).coeff k = u
theorem polynomial.trinomial_nat_degree {R : Type u_1} [semiring R] {k m n : } {u v w : R} (hkm : k < m) (hmn : m < n) (hw : w 0) :
n u v w).nat_degree = n
theorem polynomial.trinomial_nat_trailing_degree {R : Type u_1} [semiring R] {k m n : } {u v w : R} (hkm : k < m) (hmn : m < n) (hu : u 0) :
theorem polynomial.trinomial_leading_coeff {R : Type u_1} [semiring R] {k m n : } {u v w : R} (hkm : k < m) (hmn : m < n) (hw : w 0) :
n u v w).leading_coeff = w
theorem polynomial.trinomial_trailing_coeff {R : Type u_1} [semiring R] {k m n : } {u v w : R} (hkm : k < m) (hmn : m < n) (hu : u 0) :
n u v w).trailing_coeff = u
theorem polynomial.trinomial_monic {R : Type u_1} [semiring R] {k m n : } {u v : R} (hkm : k < m) (hmn : m < n) :
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) :
n u v w).mirror = (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) :
n u v w).support = {k, m, n}

A unit trinomial is a trinomial with unit coefficients.

Equations
theorem polynomial.is_unit_trinomial.irreducible_aux1 {p : polynomial } {k m n : } (hkm : k < m) (hmn : m < n) (u v w : ˣ) (hp : p = n u v w) :
* * polynomial.X ^ (m + n) + * polynomial.X ^ (n - m + k + n)) = {to_finsupp := finsupp.filter (set.Ioo (k + n) (n + n)) (p * p.mirror).to_finsupp}
theorem polynomial.is_unit_trinomial.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 = n u v w) (hq : q = n u v w) (h : p * p.mirror = q * q.mirror) :
q = p q = p.mirror
theorem polynomial.is_unit_trinomial.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 = n u v w) (hq : q = n x v z) (h : p * p.mirror = q * q.mirror) :
q = p q = p.mirror

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

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