Def Mathlib.Meta.delabFinsetFilter

Modification history

2025-11-19 06:07
Mathlib/Data/Fintype/Defs.lean
chore: move Mathlib to the module system (#31786) …
Deleted Mathlib.Meta.delabFinsetFilterView on Github →
2025-03-21 21:43
Mathlib/Data/Fintype/Defs.lean
feat: delaborator for finset builder notation (#22076)
Added Mathlib.Meta.delabFinsetFilterView on Github →