refactor(data/finsupp/basic): split data/finsupp/basic into three p…

…arts (#15699) This PR splits the ~2900 lines of `data/finsupp/basic` into more manageable parts: * the most basic material (~1000 lines) moves to `data/finsupp/defs` * lemmas about `finsupp.sum` and `finsupp.prod` move to `algebra/big_operators/finsupp` * the remaining less-used definitions and lemmas remain in `data/finsupp/basic` (~1600 lines)
leanprover-community · Aug 19, 2022 · f9c3000 · f9c3000
1 parent 0fc5496
commit f9c3000
Show file tree

Hide file tree

Showing 17 changed files with 1,629 additions and 1,549 deletions.
diff --git a/src/algebra/big_operators/associated.lean b/src/algebra/big_operators/associated.lean
@@ -5,8 +5,7 @@ Authors: Johannes Hölzl, Jens Wagemaker, Anne Baanen
 -/
 
 import algebra.associated
-import algebra.big_operators.basic
-import data.finsupp.basic
+import algebra.big_operators.finsupp
 
 /-!
 # Products of associated, prime, and irreducible elements.

diff --git a/src/algebra/big_operators/finsupp.lean b/src/algebra/big_operators/finsupp.lean
diff --git a/src/data/finset/finsupp.lean b/src/data/finset/finsupp.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
+import algebra.big_operators.finsupp
 import data.finset.pointwise
 import data.finsupp.indicator
 import data.fintype.card

diff --git a/src/data/finsupp/basic.lean b/src/data/finsupp/basic.lean
diff --git a/src/data/finsupp/big_operators.lean b/src/data/finsupp/big_operators.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yakov Pechersky
 -/
 
-import data.finsupp.basic
+import data.finsupp.defs
 
 /-!
 

diff --git a/src/data/finsupp/default.lean b/src/data/finsupp/default.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
-import data.finsupp.basic
+import data.finsupp.defs
 /-!
   # Default finsupp file
   This file imports `data.finsupp.basic`