feat: MvPolynomial.degreeOf_C_mul (#11073)

Adds lemma about the degree of a polynomial multiplied by a constant.

Mathlib/Data/MvPolynomial/Variables.lean

@@ -566,6 +566,18 @@ theorem degreeOf_mul_X_eq (j : σ) (f : MvPolynomial σ R) :
 set_option linter.uppercaseLean3 false in
 #align mv_polynomial.degree_of_mul_X_eq MvPolynomial.degreeOf_mul_X_eq
 
+theorem degreeOf_C_mul_le (p : MvPolynomial σ R) (i : σ) (c : R) :
+    (C c * p).degreeOf i ≤ p.degreeOf i := by
+  unfold degreeOf
+  convert Multiset.count_le_of_le i <| degrees_mul (C c) p
+  simp [degrees_C]
+
+theorem degreeOf_mul_C_le (p : MvPolynomial σ R) (i : σ) (c : R) :
+    (p * C c).degreeOf i ≤ p.degreeOf i := by
+  unfold degreeOf
+  convert Multiset.count_le_of_le i <| degrees_mul p (C c)
+  simp [degrees_C]
+
 theorem degreeOf_rename_of_injective {p : MvPolynomial σ R} {f : σ → τ} (h : Function.Injective f)
     (i : σ) : degreeOf (f i) (rename f p) = degreeOf i p := by
   classical