feat: port Data.Finset.Lattice (#1606)

Co-authored-by: agjftucker <agjftucker@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
leanprover-community · Jan 17, 2023 · 94cbe78 · 94cbe78
1 parent c2c17ab
commit 94cbe78
Show file tree

Hide file tree

Showing 2 changed files with 1,987 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -232,6 +232,7 @@ import Mathlib.Data.Finset.Card
 import Mathlib.Data.Finset.Fin
 import Mathlib.Data.Finset.Fold
 import Mathlib.Data.Finset.Image
+import Mathlib.Data.Finset.Lattice
 import Mathlib.Data.Finset.NAry
 import Mathlib.Data.Finset.Option
 import Mathlib.Data.Finset.Order