Commit 2024-02-11 05:41 841bef78
View on Github →feat: add Prime.not_dvd_finset_prod and Prime.not_dvd_finsupp_prod (#10047)
We already have Prime.not_dvd_prod
, which is about list products: https://github.com/leanprover-community/mathlib4/blob/1fec3c4a56a0a991f7324bb7b1f89ab6a6795d19/Mathlib/Data/List/Prime.lean#L41-L43
This PR adds analogous theorems for Finset
and Finsupp
.