From 2f9397b97fa959693981d818ae745ad776186166 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sat, 2 Mar 2024 09:06:35 +0000
Subject: [PATCH] feat: MvPolynomial.degreeOf_C_mul (#11073)

Adds lemma about the degree of a polynomial multiplied by a constant.
---
 Mathlib/Data/MvPolynomial/Variables.lean | 12 ++++++++++++
 1 file changed, 12 insertions(+)

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