Polynomials of specific degree #
Facts about polynomials that have a specific integer degree.
theorem
Polynomial.Monic.irreducible_iff_roots_eq_zero_of_degree_le_three
{R : Type u_1}
[CommRing R]
[IsDomain R]
{p : Polynomial R}
(hp : Polynomial.Monic p)
(hp2 : 2 ≤ Polynomial.natDegree p)
(hp3 : Polynomial.natDegree p ≤ 3)
:
Irreducible p ↔ Polynomial.roots p = 0
A polynomial of degree 2 or 3 is irreducible iff it doesn't have roots.
theorem
Polynomial.irreducible_iff_roots_eq_zero_of_degree_le_three
{K : Type u_1}
[Field K]
{p : Polynomial K}
(hp2 : 2 ≤ Polynomial.natDegree p)
(hp3 : Polynomial.natDegree p ≤ 3)
:
Irreducible p ↔ Polynomial.roots p = 0
A polynomial of degree 2 or 3 is irreducible iff it doesn't have roots.