Some lemmas about the degree lexicographic monomial order on multivariate polynomials

theorem MvPolynomial.degree_degLexDegree {σ : Type u_1} {R : Type u_2} [CommSemiring R] {f : MvPolynomial σ R} [LinearOrder σ] [WellFoundedGT σ] : Finsupp.degree (MonomialOrder.degLex.degree f) = f.totalDegree

theorem MvPolynomial.degLex_totalDegree_monotone {σ : Type u_1} {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} [LinearOrder σ] [WellFoundedGT σ] (h : MonomialOrder.degLex.toSyn (MonomialOrder.degLex.degree f) ≤ MonomialOrder.degLex.toSyn (MonomialOrder.degLex.degree g)) : f.totalDegree ≤ g.totalDegree

theorem MvPolynomial.totalDegree_mul_of_isDomain {σ : Type u_1} {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} [NoZeroDivisors R] (hf : f ≠ 0) (hg : g ≠ 0) : (f * g).totalDegree = f.totalDegree + g.totalDegree

theorem MvPolynomial.totalDegree_le_of_dvd_of_isDomain {σ : Type u_1} {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} [NoZeroDivisors R] (h : f ∣ g) (hg : g ≠ 0) : f.totalDegree ≤ g.totalDegree

theorem MvPolynomial.dvd_C_iff_exists {σ : Type u_1} {R : Type u_2} [CommSemiring R] {f : MvPolynomial σ R} [NoZeroDivisors R] {a : R} (ha : a ≠ 0) : f ∣ C a ↔ ∃ (b : R), b ∣ a ∧ f = C b

theorem MvPolynomial.dvd_monomial_iff_exists {σ : Type u_1} {R : Type u_2} [CommRing R] [NoZeroDivisors R] {p : MvPolynomial σ R} {n : σ →₀ ℕ} {a : R} (ha : a ≠ 0) : p ∣ (monomial n) a ↔ ∃ (m : σ →₀ ℕ) (b : R), m ≤ n ∧ b ∣ a ∧ p = (monomial m) b

theorem MvPolynomial.dvd_monomial_one_iff_exists {σ : Type u_1} {R : Type u_2} [CommRing R] [NoZeroDivisors R] {p : MvPolynomial σ R} {n : σ →₀ ℕ} : p ∣ (monomial n) 1 ↔ ∃ (m : σ →₀ ℕ) (u : R), m ≤ n ∧ IsUnit u ∧ p = (monomial m) u

theorem MvPolynomial.dvd_X_iff_exists {σ : Type u_1} {R : Type u_2} [CommRing R] [NoZeroDivisors R] {p : MvPolynomial σ R} {i : σ} : p ∣ X i ↔ ∃ (r : R), IsUnit r ∧ (p = C r ∨ p = r • X i)