mathlib documentation

data.polynomial.unit_trinomial

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

Shorthand for a trinomial

Equations
theorem polynomial.trinomial_leading_coeff' {R : Type u_1} [semiring R] {k m n : } {u v 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 v 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 v w : R} (hkm : k < m) (hmn : m < n) :
(polynomial.trinomial k m 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) :
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) :
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) :
theorem polynomial.trinomial_monic {R : Type u_1} [semiring R] {k m n : } {u v : R} (hkm : k < m) (hmn : m < n) :
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) :
(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 v 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
theorem polynomial.is_unit_trinomial.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) :
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 = 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.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 = 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

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