diff --git a/library/data/int/div.lean b/library/data/int/div.lean
index d23eef584..add7a9679 100644
--- a/library/data/int/div.lean
+++ b/library/data/int/div.lean
@@ -11,7 +11,6 @@ import data.int.order data.nat.div
 open [coercions] [reduce-hints] nat
 open [declarations] nat (succ)
 open eq.ops
-notation `ℕ` := nat
 
 namespace int
 
diff --git a/library/init/nat.lean b/library/init/nat.lean
index 18e4f1dbc..8ac028be3 100644
--- a/library/init/nat.lean
+++ b/library/init/nat.lean
@@ -7,8 +7,9 @@ prelude
 import init.wf init.tactic init.num
 open eq.ops decidable or
 
+notation `ℕ` := nat
+
 namespace nat
-  notation `ℕ` := nat
 
   /- basic definitions on natural numbers -/
   inductive le (a : ℕ) : ℕ → Prop :=