mathlib3
90755c36 - refactor(order/filter/ultrafilter): drop `filter.is_ultrafilter` (#5264)

Commit
5 years ago
refactor(order/filter/ultrafilter): drop `filter.is_ultrafilter` (#5264) Use bundled `ultrafilter`s instead.
Author
Parents
Loading