Commit 2022-01-03 11:27 a10cb2f3

View on Github →

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.

Estimated changes

Modified src/algebra/big_operators/associated.lean

added theorem nat.prime.dvd_finset_prod_iff

added theorem nat.prime.dvd_finsupp_prod_iff

added theorem prime.dvd_finset_prod_iff

added theorem prime.dvd_finsupp_prod_iff

modified theorem prime.dvd_prod_iff