refactor(logic/schroeder_bernstein): move to set_theory/ (#599)

leanprover-community · Jan 15, 2019 · 024da40 · 024da40
1 parent d4f80f6
commit 024da40
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 1 deletion.
diff --git a/src/set_theory/cardinal.lean b/src/set_theory/cardinal.lean
@@ -8,7 +8,7 @@ Cardinal arithmetic.
 Cardinals are represented as quotient over equinumerous types.
 -/
 
-import data.set.finite data.quot logic.schroeder_bernstein logic.function
+import data.set.finite data.quot logic.function set_theory.schroeder_bernstein
 
 open function lattice set
 local attribute [instance] classical.prop_decidable

diff --git a/src/logic/schroeder_bernstein.lean → src/set_theory/schroeder_bernstein.lean b/src/logic/schroeder_bernstein.lean → src/set_theory/schroeder_bernstein.lean