diff --git a/library/data/nat/default.lean b/library/data/nat/default.lean index 8d81f519f..ca7ef3aa9 100644 --- a/library/data/nat/default.lean +++ b/library/data/nat/default.lean @@ -3,4 +3,4 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Jeremy Avigad -/ -import .basic .order .sub .div .gcd .bquant .sqrt .pairing .power .choose .fact .primes +import .basic .order .sub .div .gcd .bquant .sqrt .pairing .power .choose .fact .parity diff --git a/library/theories/number_theory/bezout.lean b/library/theories/number_theory/bezout.lean index 8608a0527..349a942e0 100644 --- a/library/theories/number_theory/bezout.lean +++ b/library/theories/number_theory/bezout.lean @@ -5,7 +5,7 @@ Authors: William Peterson, Jeremy Avigad Extended gcd, Bezout's theorem, chinese remainder theorem. -/ -import data.nat.div data.int data.nat.primes +import data.nat.div data.int .primes /- Bezout's theorem -/ diff --git a/library/data/nat/primes.lean b/library/theories/number_theory/primes.lean similarity index 98% rename from library/data/nat/primes.lean rename to library/theories/number_theory/primes.lean index ce20e41bd..af2c2850f 100644 --- a/library/data/nat/primes.lean +++ b/library/theories/number_theory/primes.lean @@ -5,7 +5,7 @@ Authors: Leonardo de Moura Prime numbers -/ -import data.nat.fact data.nat.gcd data.nat.bquant data.nat.power data.nat.parity logic.identities +import data.nat logic.identities open bool namespace nat