feat: port Mathlib.Data.Ordmap.Ordnode (#1455)

Co-authored-by: Arien Malec <arien.malec@gmail.com> Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com> Co-authored-by: Moritz Firsching <firsching@google.com> Co-authored-by: qawbecrdtey <qawbecrdtey@kaist.ac.kr>
leanprover-community · May 1, 2023 · 0ed9c8d · 0ed9c8d
1 parent 7b35d8f
commit 0ed9c8d
Show file tree

Hide file tree

Showing 3 changed files with 1,366 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1055,6 +1055,7 @@ import Mathlib.Data.Opposite
 import Mathlib.Data.Option.Basic
 import Mathlib.Data.Option.Defs
 import Mathlib.Data.Option.NAry
+import Mathlib.Data.Ordmap.Ordnode
 import Mathlib.Data.PEquiv
 import Mathlib.Data.PFun
 import Mathlib.Data.PFunctor.Multivariate.Basic