Commit 2022-01-30 14:09 02c720ee

chore(*): Rename prod_dvd_prod (#11734) In #11693 I introduced the counterpart for multiset of finset.prod_dvd_prod. It makes sense for these to have the same name, but there's already a different lemma called multiset.prod_dvd_prod, so the new lemma was named multiset.prod_dvd_prod_of_dvd instead. As discussed with @riccardobrasca and @ericrbg at #11693, this PR brings the names of the two counterpart lemmas into alignment, and also renames multiset.prod_dvd_prod to something more informative. Renaming as follows: multiset.prod_dvd_prod to multiset.prod_dvd_prod_of_le finset.prod_dvd_prod to finset.prod_dvd_prod_of_dvd