feat: port Order.Atoms (#1257)

- [ ] depends on: #1258 Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
leanprover-community · Dec 30, 2022 · 8618f40 · 8618f40
1 parent 879a327
commit 8618f40
Show file tree

Hide file tree

Showing 2 changed files with 939 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -403,6 +403,7 @@ import Mathlib.Mathport.Rename
 import Mathlib.Mathport.Syntax
 import Mathlib.Order.Antichain
 import Mathlib.Order.Antisymmetrization
+import Mathlib.Order.Atoms
 import Mathlib.Order.Basic
 import Mathlib.Order.BooleanAlgebra
 import Mathlib.Order.Bounded