A factor of a homogeneous polynomial is homogeneous

A candidate for Mathlib.RingTheory.MvPolynomial.Homogeneous: over a commutative semiring without zero divisors, a factor φ of a homogeneous polynomial φ * ψ with ψ ≠ 0 is homogeneous, of degree its total degree (MvPolynomial.IsHomogeneous.of_mul_left).

The proof compares the least and the largest degree of the monomials of a polynomial: its order as a power series, which is additive in a product (MvPowerSeries.order_mul), and its total degree, which is additive too (MvPolynomial.totalDegree_mul_of_isDomain). In a homogeneous product the two sums agree, so each factor has its least degree equal to its largest. Mathlib's file imports neither of the two additivity results.

theorem MvPolynomial.IsHomogeneous.of_mul_left {σ : Type u_1} {R : Type u_2} [CommSemiring R] {φ ψ : MvPolynomial σ R} {n : ℕ} [NoZeroDivisors R] (h : (φ * ψ).IsHomogeneous n) (hψ : ψ ≠ 0) : φ.IsHomogeneous φ.totalDegree

A factor φ of a homogeneous polynomial φ * ψ with ψ ≠ 0, over a semiring without zero divisors, is homogeneous: in a product the least degrees of the monomials add up, and so do the largest.