feat: port Algebra.BigOperators.Finsupp (#1900)

Some simpNF issues & some leaky classicals caused trouble. But done now!
leanprover-community · Jan 30, 2023 · 62a7ce4 · 62a7ce4
1 parent d389d10
commit 62a7ce4
Show file tree

Hide file tree

Showing 2 changed files with 648 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -2,6 +2,7 @@ import Mathlib.Algebra.Abs
 import Mathlib.Algebra.Associated
 import Mathlib.Algebra.BigOperators.Basic
 import Mathlib.Algebra.BigOperators.Finprod
+import Mathlib.Algebra.BigOperators.Finsupp
 import Mathlib.Algebra.BigOperators.Intervals
 import Mathlib.Algebra.BigOperators.Multiset.Basic
 import Mathlib.Algebra.BigOperators.Multiset.Lemmas