Unit Trinomials #
This file defines irreducible trinomials and proves an irreducibility criterion.
Main definitions #
Main results #
Polynomial.IsUnitTrinomial.irreducible_of_coprime
: An irreducibility criterion for unit trinomials.
Shorthand for a trinomial
Equations
Instances For
A unit trinomial is a trinomial with unit coefficients.
Equations
Instances For
theorem
Polynomial.IsUnitTrinomial.coeff_isUnit
{p : Polynomial ℤ}
(hp : p.IsUnitTrinomial)
{k : ℕ}
(hk : k ∈ p.support)
:
theorem
Polynomial.IsUnitTrinomial.leadingCoeff_isUnit
{p : Polynomial ℤ}
(hp : p.IsUnitTrinomial)
:
theorem
Polynomial.IsUnitTrinomial.trailingCoeff_isUnit
{p : Polynomial ℤ}
(hp : p.IsUnitTrinomial)
:
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