mathlib
20f97964 - feat(algebra/big_operators): add lemmas about sum of disjoint multiset (#15556)

Commit

3 years ago

feat(algebra/big_operators): add lemmas about sum of disjoint multiset (#15556) Some easy lemmas about sum of disjoint ```multiset``` are proved.

Author

xroblot

Parents