Commit 2024-12-02 15:15 612f6c3a

View on Github →

feat(Algebra/BigOperators/Ring): add Multiset.sum_map_div lemma (#19630)

Estimated changes

Modified Mathlib/Algebra/BigOperators/Ring.lean

added theorem Multiset.sum_map_div