diff --git a/Mathlib/Algebra/MvPolynomial/Basic.lean b/Mathlib/Algebra/MvPolynomial/Basic.lean
index be6945f8eee797..8adbbe2b52383d 100644
--- a/Mathlib/Algebra/MvPolynomial/Basic.lean
+++ b/Mathlib/Algebra/MvPolynomial/Basic.lean
@@ -290,6 +290,10 @@ theorem monomial_sum_index {α : Type*} (s : Finset α) (f : α → σ →₀ 
     monomial (∑ i ∈ s, f i) a = C a * ∏ i ∈ s, monomial (f i) 1 := by
   rw [← monomial_sum_one, C_mul', ← (monomial _).map_smul, smul_eq_mul, mul_one]
 
+theorem monomial_sum_eq_prod {α : Type*} (s : Finset α) (f : α → σ →₀ ℕ) (g : α → R) :
+    monomial (∑ i ∈ s, f i) (∏ i ∈ s, g i) = ∏ i ∈ s, monomial (f i) (g i) := by
+  simp_rw [monomial_sum_index, map_prod, ← Finset.prod_mul_distrib, C_mul_monomial, mul_one]
+
 theorem monomial_finsupp_sum_index {α β : Type*} [Zero β] (f : α →₀ β) (g : α → β → σ →₀ ℕ)
     (a : R) : monomial (f.sum g) a = C a * f.prod fun a b => monomial (g a b) 1 :=
   monomial_sum_index _ _ _