Unit Trinomials #
This file defines irreducible trinomials and proves an irreducibility criterion.
Main definitions #
Main results #
polynomial.irreducible_of_coprime
: An irreducibility criterion for unit trinomials.
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 v 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 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) :
(polynomial.trinomial k m 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) :
(polynomial.trinomial k m n u v w).nat_trailing_degree = k
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) :
(polynomial.trinomial k m 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) :
(polynomial.trinomial k m 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) :
(polynomial.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) :
(polynomial.trinomial k m n u v w).mirror = polynomial.trinomial k (n - m + k) n w v u
A unit trinomial is a trinomial with unit coefficients.
theorem
polynomial.is_unit_trinomial.card_support_eq_three
{p : polynomial ℤ}
(hp : p.is_unit_trinomial) :
theorem
polynomial.is_unit_trinomial.coeff_is_unit
{p : polynomial ℤ}
(hp : p.is_unit_trinomial)
{k : ℕ}
(hk : k ∈ p.support) :
theorem
polynomial.is_unit_trinomial.leading_coeff_is_unit
{p : polynomial ℤ}
(hp : p.is_unit_trinomial) :
theorem
polynomial.is_unit_trinomial.trailing_coeff_is_unit
{p : polynomial ℤ}
(hp : p.is_unit_trinomial) :
theorem
polynomial.is_unit_trinomial_iff'
{p : polynomial ℤ} :
p.is_unit_trinomial ↔ (p * p.mirror).coeff (((p * p.mirror).nat_degree + (p * p.mirror).nat_trailing_degree) / 2) = 3
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) :
⇑polynomial.C ↑v * (⇑polynomial.C ↑u * polynomial.X ^ (m + n) + ⇑polynomial.C ↑w * 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_of_coprime
{p : polynomial ℤ}
(hp : p.is_unit_trinomial)
(h : ∀ (q : polynomial ℤ), q ∣ p → q ∣ p.mirror → is_unit q) :
theorem
polynomial.is_unit_trinomial.irreducible_of_is_coprime
{p : polynomial ℤ}
(hp : p.is_unit_trinomial)
(h : is_coprime p p.mirror) :
A unit trinomial is irreducible if it is coprime with its mirror
theorem
polynomial.is_unit_trinomial.irreducible_of_coprime'
{p : polynomial ℤ}
(hp : p.is_unit_trinomial)
(h : ∀ (z : ℂ), ¬(⇑(polynomial.aeval z) p = 0 ∧ ⇑(polynomial.aeval z) p.mirror = 0)) :
A unit trinomial is irreducible if it has no complex roots in common with its mirror