mathlib3 documentation

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 #

Main results #

source
noncomputable def polynomial.trinomial {R : Type u_1} [semiring R] (k m n : ℕ) (u v w : R) :
polynomial R

Shorthand for a trinomial

Equations
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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}
source
def polynomial.is_unit_trinomial (p : polynomial ℤ) :
Prop

A unit trinomial is a trinomial with unit coefficients.

Equations
source
theorem polynomial.is_unit_trinomial.not_is_unit {p : polynomial ℤ} (hp : p.is_unit_trinomial) :
¬is_unit p
source
theorem polynomial.is_unit_trinomial.card_support_eq_three {p : polynomial ℤ} (hp : p.is_unit_trinomial) :
p.support.card = 3
source
theorem polynomial.is_unit_trinomial.ne_zero {p : polynomial ℤ} (hp : p.is_unit_trinomial) :
p ≠ 0
source
theorem polynomial.is_unit_trinomial.coeff_is_unit {p : polynomial ℤ} (hp : p.is_unit_trinomial) {k : ℕ} (hk : k ∈ p.support) :
is_unit (p.coeff k)
source
theorem polynomial.is_unit_trinomial.leading_coeff_is_unit {p : polynomial ℤ} (hp : p.is_unit_trinomial) :
is_unit p.leading_coeff
source
theorem polynomial.is_unit_trinomial.trailing_coeff_is_unit {p : polynomial ℤ} (hp : p.is_unit_trinomial) :
is_unit p.trailing_coeff
source
theorem polynomial.is_unit_trinomial_iff {p : polynomial ℤ} :
p.is_unit_trinomial ↔ p.support.card = 3 ∧ ∀ (k : ℕ), k ∈ p.support → is_unit (p.coeff k)
source
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
source
theorem polynomial.is_unit_trinomial_iff'' {p q : polynomial ℤ} (h : p * p.mirror = q * q.mirror) :
p.is_unit_trinomial ↔ q.is_unit_trinomial
source
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}
source
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
source
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
source
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) :
irreducible p
source
theorem polynomial.is_unit_trinomial.irreducible_of_is_coprime {p : polynomial ℤ} (hp : p.is_unit_trinomial) (h : is_coprime p p.mirror) :
irreducible p

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

source
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)) :
irreducible p

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