Commit 2025-03-21 21:43 e0a85d79

View on Github →

feat: delaborator for finset builder notation (#22076)

Estimated changes

Modified Mathlib/Algebra/BigOperators/Expect.lean

Modified Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean

Modified Mathlib/Data/Fintype/Defs.lean

added def Mathlib.Meta.delabFinsetFilter

Created MathlibTest/Delab/FinsetBuilder.lean