chore(logic/equiv/basic): split into two files (#17038)

A fairly easy split of `logic.equiv.basic` into `logic.equiv.defs` (containing the stuff with very little prerequisites, and which suffices for many other files), and `logic.equiv.basic` (the stuff that requires other imports from around `logic.*`). `logic.equiv.basic` is still a ~1500 line file, so I'd like to split it further shortly. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
leanprover-community · Oct 18, 2022 · 9407b03 · 9407b03
1 parent 8c9b005
commit 9407b03
Show file tree

Hide file tree

Showing 29 changed files with 853 additions and 820 deletions.
diff --git a/src/algebra/free.lean b/src/algebra/free.lean
@@ -6,7 +6,7 @@ Authors: Kenny Lau
 import algebra.hom.group
 import control.applicative
 import control.traversable.basic
-import logic.equiv.basic
+import logic.equiv.defs
 
 /-!
 # Free constructions

diff --git a/src/algebra/group/type_tags.lean b/src/algebra/group/type_tags.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import algebra.hom.group
-import logic.equiv.basic
+import logic.equiv.defs
 import data.finite.defs
 /-!
 # Type tags that turn additive structures into multiplicative, and vice versa

diff --git a/src/algebra/group/with_one.lean b/src/algebra/group/with_one.lean
@@ -5,7 +5,7 @@ Authors: Mario Carneiro, Johan Commelin
 -/
 import algebra.hom.equiv
 import algebra.ring.basic
-import logic.equiv.basic
+import logic.equiv.defs
 import logic.equiv.option
 
 /-!

diff --git a/src/algebra/opposites.lean b/src/algebra/opposites.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 -/
 import algebra.group.defs
-import logic.equiv.basic
+import logic.equiv.defs
 import logic.nontrivial
 
 /-!

diff --git a/src/category_theory/functor/fully_faithful.lean b/src/category_theory/functor/fully_faithful.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import category_theory.natural_isomorphism
-import logic.equiv.basic
+import logic.equiv.defs
 
 /-!
 # Full and faithful functors

diff --git a/src/category_theory/types.lean b/src/category_theory/types.lean
@@ -5,7 +5,7 @@ Authors: Stephen Morgan, Scott Morrison, Johannes Hölzl
 -/
 import category_theory.epi_mono
 import category_theory.functor.fully_faithful
-import logic.equiv.basic
+import logic.equiv.defs
 
 /-!
 # The category `Type`.

diff --git a/src/combinatorics/derangements/basic.lean b/src/combinatorics/derangements/basic.lean
@@ -5,7 +5,7 @@ Authors: Henry Swanson
 -/
 import dynamics.fixed_points.basic
 import group_theory.perm.option
-import logic.equiv.basic
+import logic.equiv.defs
 import logic.equiv.option
 
 /-!

diff --git a/src/control/equiv_functor.lean b/src/control/equiv_functor.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import logic.equiv.basic
+import logic.equiv.defs
 
 /-!
 # Functions functorial with respect to equivalences

diff --git a/src/control/monad/basic.lean b/src/control/monad/basic.lean
@@ -3,7 +3,7 @@ Copyright (c) 2019 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon
 -/
-import logic.equiv.basic
+import logic.equiv.defs
 import tactic.basic
 
 /-!

diff --git a/src/control/monad/writer.lean b/src/control/monad/writer.lean
@@ -6,7 +6,7 @@ Authors: Simon Hudon
 The writer monad transformer for passing immutable state.
 -/
 import algebra.group.defs
-import logic.equiv.basic
+import logic.equiv.defs
 
 universes u v w u₀ u₁ v₀ v₁
 

diff --git a/src/control/traversable/equiv.lean b/src/control/traversable/equiv.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon
 -/
 import control.traversable.lemmas
-import logic.equiv.basic
+import logic.equiv.defs
 
 /-!
 # Transferring `traversable` instances along isomorphisms

diff --git a/src/data/erased.lean b/src/data/erased.lean
@@ -3,7 +3,7 @@ Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import logic.equiv.basic
+import logic.equiv.defs
 
 /-!
 # A type for VM-erased data

diff --git a/src/data/opposite.lean b/src/data/opposite.lean
@@ -3,7 +3,7 @@ Copyright (c) 2018 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Reid Barton, Simon Hudon, Kenny Lau
 -/
-import logic.equiv.basic
+import logic.equiv.defs
 
 /-!
 # Opposites

diff --git a/src/data/part.lean b/src/data/part.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Jeremy Avigad, Simon Hudon
 -/
 import data.set.basic
-import logic.equiv.basic
+import logic.equiv.defs
 
 /-!
 # Partial values of a type

diff --git a/src/logic/embedding.lean b/src/logic/embedding.lean
@@ -7,7 +7,7 @@ import data.fun_like.embedding
 import data.prod.pprod
 import data.set.basic
 import data.sigma.basic
-import logic.equiv.basic
+import logic.equiv.defs
 
 /-!
 # Injective functions