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.

theorem Polynomial.irreducible_of_degree_le_three_of_not_isRoot {K : Type u_1} [Field K] {p : Polynomial K} (hdeg : p.natDegree ∈ Finset.Icc 1 3) (hnot : ∀ (x : K), ¬p.IsRoot x) : Irreducible p