mathlib3
8fcb820b - feat(order/filter/basic): add `filter.has_basis.bInter_mem` (#15661)

Commit
3 years ago
feat(order/filter/basic): add `filter.has_basis.bInter_mem` (#15661) Use it to golf a few proofs.
Author
Parents
Loading