feat(RingTheory/MvPolynomial/MonomialOrder): add leadingTerm_mul lemma (#37471)

Co-authored-by: NoahW314 <noahwalker3.14@gmail.com>

Author: NoahW314

Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean

@@ -802,6 +802,13 @@ lemma leadingTerm_eq_leadingTerm_iff {p q : MvPolynomial σ R} :
   rw [leadingTerm, leadingTerm, monomial_eq_monomial_iff]
   aesop
 
+@[simp]
+theorem leadingTerm_mul [NoZeroDivisors R] (p q : MvPolynomial σ R) :
+    m.leadingTerm (p * q) = m.leadingTerm p * m.leadingTerm q := by
+  by_cases! h0 : p * q = 0
+  · simp [h0, zero_eq_mul.mp]
+  simp [leadingTerm, m.degree_mul' h0]
+
 @[simp, nontriviality]
 lemma monic_of_subsingleton [Subsingleton R] (p : MvPolynomial σ R) :
     m.Monic p := by