feat: Components of Multiset.prod over α × β (#12655)

Mathlib/Algebra/BigOperators/Multiset/Lemmas.lean

@@ -5,17 +5,18 @@ Authors: Chris Hughes, Bhavik Mehta, Eric Wieser
 -/
 import Mathlib.Algebra.BigOperators.List.Lemmas
 import Mathlib.Algebra.BigOperators.Multiset.Basic
+import Mathlib.Algebra.Group.Prod
 
 #align_import algebra.big_operators.multiset.lemmas from "leanprover-community/mathlib"@"0a0ec35061ed9960bf0e7ffb0335f44447b58977"
 
 /-! # Lemmas about `Multiset.sum` and `Multiset.prod` requiring extra algebra imports -/
 
 
-variable {α : Type*}
+variable {α β : Type*}
 
 namespace Multiset
 section CommMonoid
-variable [CommMonoid α] {s : Multiset α} {a : α}
+variable [CommMonoid α] [CommMonoid β] {s : Multiset α} {a : α}
 
 lemma dvd_prod : a ∈ s → a ∣ s.prod :=
   Quotient.inductionOn s (fun l a h => by simpa using List.dvd_prod h) a
@@ -25,6 +26,12 @@ lemma dvd_prod : a ∈ s → a ∣ s.prod :=
     (s.map Neg.neg).prod = (-1) ^ card s * s.prod := Quotient.inductionOn s (by simp)
 #align multiset.prod_map_neg Multiset.prod_map_neg
 
+@[to_additive] lemma fst_prod (s : Multiset (α × β)) : s.prod.1 = (s.map Prod.fst).prod :=
+  map_multiset_prod (MonoidHom.fst _ _) _
+
+@[to_additive] lemma snd_prod (s : Multiset (α × β)) : s.prod.2 = (s.map Prod.snd).prod :=
+  map_multiset_prod (MonoidHom.snd _ _) _
+
 end CommMonoid
 
 section CommMonoidWithZero