Skip to content

Commit 218a453

Browse files
committed
Feat: port Order.Filter.Bases (#1791)
1 parent 8992742 commit 218a453

File tree

3 files changed

+1219
-3
lines changed

3 files changed

+1219
-3
lines changed

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -653,6 +653,7 @@ import Mathlib.Order.Cover
653653
import Mathlib.Order.Directed
654654
import Mathlib.Order.Disjoint
655655
import Mathlib.Order.Extension.Linear
656+
import Mathlib.Order.Filter.Bases
656657
import Mathlib.Order.Filter.Basic
657658
import Mathlib.Order.Filter.CountableInter
658659
import Mathlib.Order.Filter.Curry

0 commit comments

Comments
 (0)