mathlib3
53a484e6 - chore(order/filter/small_sets): redefine, golf (#13672)

Commit
3 years ago
chore(order/filter/small_sets): redefine, golf (#13672) The new definition is defeq to the old one.
Author
Parents
Loading