diff --git a/Mathlib/Data/MvPolynomial/Variables.lean b/Mathlib/Data/MvPolynomial/Variables.lean
index c8ce16d44cb0c..486df48dbb3d7 100644
--- a/Mathlib/Data/MvPolynomial/Variables.lean
+++ b/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