Odd-degree irreducible factors

An odd-degree polynomial has an irreducible factor of odd degree over any commutative semiring without zero divisors in which strict divisibility is well-founded.

theorem Polynomial.exists_irreducible_factor_of_odd_natDegree {K : Type u_1} [CommSemiring K] [NoZeroDivisors K] [WfDvdMonoid K] (p : Polynomial K) (hp : Odd p.natDegree) : ∃ (q : Polynomial K), Irreducible q ∧ Odd q.natDegree ∧ q ∣ p

An odd-degree polynomial has an odd-degree irreducible factor.