Commit 2023-03-17 15:21 5180019b

View on Github →

feat: finset.sum under mod (#2025) Match https://github.com/leanprover-community/mathlib/pull/18364

Estimated changes

added theorem Finset.prod_int_mod
added theorem Finset.prod_nat_mod
added theorem Finset.sum_int_mod
added theorem Finset.sum_nat_mod
added theorem Multiset.prod_int_mod
added theorem Multiset.prod_nat_mod
added theorem Multiset.sum_int_mod
added theorem Multiset.sum_nat_mod