Commit 2026-08-25 15:52 e995b77c

View on Github →

refactor(Data/Multiset): rename map_filter' (#42970) The deprecated alias was removed in https://github.com/leanprover-community/mathlib4/pull/21271.

Estimated changes

Modified Mathlib/Data/Multiset/Filter.lean

deleted theorem Multiset.map_filter'

added theorem Multiset.map_filter