split(data/set/prod): split off data.set.basic (#10739)

This moves `set.prod`, `set.pi` and `set.diagonal` from `data.set.basic` to a new file `data.set.prod`. I'm crediting * Mario for `set.prod` from bd013e8 * Johannes for `set.pi` from da7bbd7 * Patrick for `set.diagonal` from #3118
leanprover-community · Dec 13, 2021 · 9d73418 · 9d73418
1 parent e60899c
commit 9d73418
Show file tree

Hide file tree

Showing 9 changed files with 415 additions and 438 deletions.
diff --git a/archive/imo/imo1972_b2.lean b/archive/imo/imo1972_b2.lean
@@ -5,7 +5,6 @@ Authors: Ruben Van de Velde, Stanislas Polu
 -/
 
 import data.real.basic
-import data.set.basic
 import analysis.normed_space.basic
 
 /-!

diff --git a/archive/imo/imo2008_q2.lean b/archive/imo/imo2008_q2.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Manuel Candales
 -/
 import data.real.basic
-import data.set.basic
 import data.set.finite
 
 /-!

diff --git a/src/algebra/ring/basic.lean b/src/algebra/ring/basic.lean
@@ -6,7 +6,6 @@ Neil Strickland
 -/
 import algebra.divisibility
 import algebra.regular.basic
-import data.set.basic
 
 /-!
 # Properties and homomorphisms of semirings and rings