Commit 2023-01-13 13:17 5f003c06

View on Github →

feat: port Algebra.BigOperators.Multiset.Lemmas (#1536)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/BigOperators/Multiset/Lemmas.lean

added theorem Commute.multiset_sum_left

added theorem Commute.multiset_sum_right

added theorem Multiset.dvd_prod

added theorem Multiset.prod_eq_one_iff