associated): `dvd_prod_iff` for `finset` and `finsupp` (#10675)

Commit

3 years ago

feat(algebra/big_operators/associated): `dvd_prod_iff` for `finset` and `finsupp` (#10675) Adding the counterparts of `dvd_prod_iff` (in #10624) for `finset` and `finsupp`.

Author

stuart-presnell

Parents

a813cf5c

mathlib3 a10cb2f3 - feat(algebra/big_operators/associated): `dvd_prod_iff` for `finset` and `finsupp` (#10675)

mathlib3
a10cb2f3 - feat(algebra/big_operators/associated): `dvd_prod_iff` for `finset` and `finsupp` (#10675)