diff --git a/library/init/algebra.lean b/library/init/algebra/default.lean similarity index 59% rename from library/init/algebra.lean rename to library/init/algebra/default.lean index 811eb1e382..8681a47dea 100644 --- a/library/init/algebra.lean +++ b/library/init/algebra/default.lean @@ -4,4 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ prelude -import init.group init.ordered_group init.ring init.ordered_ring +import init.algebra.group init.algebra.ordered_group init.algebra.ring init.algebra.ordered_ring init.algebra.norm_num diff --git a/library/init/group.lean b/library/init/algebra/group.lean similarity index 100% rename from library/init/group.lean rename to library/init/algebra/group.lean diff --git a/library/init/norm_num.lean b/library/init/algebra/norm_num.lean similarity index 99% rename from library/init/norm_num.lean rename to library/init/algebra/norm_num.lean index ce18b90a64..33573967b3 100644 --- a/library/init/norm_num.lean +++ b/library/init/algebra/norm_num.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Robert Lewis and Leonardo de Moura -/ prelude -import init.ring +import init.algebra.ring namespace norm_num universe variable u diff --git a/library/init/order.lean b/library/init/algebra/order.lean similarity index 100% rename from library/init/order.lean rename to library/init/algebra/order.lean diff --git a/library/init/ordered_group.lean b/library/init/algebra/ordered_group.lean similarity index 99% rename from library/init/ordered_group.lean rename to library/init/algebra/ordered_group.lean index 5fd6ccf091..1d60509089 100644 --- a/library/init/ordered_group.lean +++ b/library/init/algebra/ordered_group.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Jeremy Avigad, Leonardo de Moura -/ prelude -import init.group +import init.algebra.order init.algebra.group /- Make sure instances defined in this file have lower priority than the ones defined for concrete structures -/ diff --git a/library/init/ordered_ring.lean b/library/init/algebra/ordered_ring.lean similarity index 99% rename from library/init/ordered_ring.lean rename to library/init/algebra/ordered_ring.lean index ef84f3b7f2..42beca9c0d 100644 --- a/library/init/ordered_ring.lean +++ b/library/init/algebra/ordered_ring.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Jeremy Avigad, Leonardo de Moura -/ prelude -import init.ordered_group init.ring +import init.algebra.ordered_group init.algebra.ring /- Make sure instances defined in this file have lower priority than the ones defined for concrete structures -/ diff --git a/library/init/ring.lean b/library/init/algebra/ring.lean similarity index 99% rename from library/init/ring.lean rename to library/init/algebra/ring.lean index 4be5b674cf..f715952b4a 100644 --- a/library/init/ring.lean +++ b/library/init/algebra/ring.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Jeremy Avigad, Leonardo de Moura -/ prelude -import init.group +import init.algebra.group /- Make sure instances defined in this file have lower priority than the ones defined for concrete structures -/ diff --git a/library/init/default.lean b/library/init/default.lean index c8d58969df..c886868af8 100644 --- a/library/init/default.lean +++ b/library/init/default.lean @@ -12,5 +12,5 @@ import init.monad init.option init.state init.fin init.list init.char init.strin import init.monad_combinators init.set import init.timeit init.trace init.unsigned init.ordering init.list_classes init.coe import init.wf init.nat_div init.meta init.instances init.breakpoint -import init.sigma_lex init.id_locked init.order init.algebra +import init.sigma_lex init.id_locked init.algebra import init.nat_lemmas init.char_lemmas init.string_lemmas diff --git a/library/init/nat.lean b/library/init/nat.lean index 87495229e6..0e06c6c97b 100644 --- a/library/init/nat.lean +++ b/library/init/nat.lean @@ -5,7 +5,6 @@ Authors: Floris van Doorn, Leonardo de Moura -/ prelude import init.relation init.num -import init.order notation `ℕ` := nat