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.

Estimated changes