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 : p.Monic)
(hp2 : 2 ≤ p.natDegree)
(hp3 : p.natDegree ≤ 3)
:
Irreducible p ↔ p.roots = 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 ≤ p.natDegree)
(hp3 : p.natDegree ≤ 3)
:
Irreducible p ↔ p.roots = 0
A polynomial of degree 2 or 3 is irreducible iff it doesn't have roots.