mathlib3
71efed1b - fix(order/filter/basic): fix a diamond (#18255)

Commit
2 years ago
fix(order/filter/basic): fix a diamond (#18255) Fix non-defeq `default` in `filter.inhabited` and `filter.unique`.
Author
Parents
Loading