Skip to content

refactor(Data/Multiset): rename map_filter' - #42970

Open
yuanyi-350 wants to merge 1 commit into
leanprover-community:masterfrom
yuanyi-350:rename-multiset-map-filter
Open

refactor(Data/Multiset): rename map_filter'#42970
yuanyi-350 wants to merge 1 commit into
leanprover-community:masterfrom
yuanyi-350:rename-multiset-map-filter

Commits

Commits on Aug 20, 2026