mathlib

de27bfc8 - feat(algebra/big_operators/{basic,multiset}): two `multiset.prod` lemmas (#11693)

feat(algebra/big_operators/{basic,multiset}): two `multiset.prod` lemmas (#11693) Two lemmas suggested by Riccardo Brasca on #11572: `to_finset_prod_dvd_prod`: `S.to_finset.prod id ∣ S.prod` `prod_dvd_prod_of_dvd`: For any `S : multiset α`, if `∀ a ∈ S, g1 a ∣ g2 a` then `S.prod g1 ∣ S.prod g2` (a counterpart to `finset.prod_dvd_prod`)