Irreducibility of unit trinomials #
TODO #
Develop more theory (e.g., it suffices to check that aeval z p ≠ 0 for z = 0 and z a root of
unity).
theorem
Polynomial.IsUnitTrinomial.irreducible_of_coprime'
{p : Polynomial ℤ}
(hp : p.IsUnitTrinomial)
(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.