feat: port Data.Finmap (#1591)

Co-authored-by: Arien Malec <arien.malec@gmail.com> Co-authored-by: qawbecrdtey <qawbecrdtey@naver.com> Co-authored-by: Komyyy <pol_tta@outlook.jp>
leanprover-community · Feb 3, 2023 · 70430c9 · 70430c9
1 parent afdc959
commit 70430c9
Show file tree

Hide file tree

Showing 2 changed files with 665 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -295,6 +295,7 @@ import Mathlib.Data.FinEnum
 import Mathlib.Data.Finite.Basic
 import Mathlib.Data.Finite.Defs
 import Mathlib.Data.Finite.Set
+import Mathlib.Data.Finmap
 import Mathlib.Data.Finset.Basic
 import Mathlib.Data.Finset.Card
 import Mathlib.Data.Finset.Fin