chore(data/nat/digits): use nat namespace (#4201)

Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
leanprover-community · Sep 21, 2020 · 92c0125 · 92c0125
1 parent 4a8c38e
commit 92c0125
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 1 deletion.
diff --git a/docs/100.yaml b/docs/100.yaml
@@ -293,7 +293,7 @@
   title  : Divisibility by 3 Rule
   author : Scott Morrison
   decls  :
-    - three_dvd_iff
+    - nat.three_dvd_iff
 86:
   title  : Lebesgue Measure and Integration
   decl   : measure_theory.lintegral

diff --git a/src/data/nat/digits.lean b/src/data/nat/digits.lean
@@ -17,6 +17,8 @@ We also prove some divisibility tests based on digits, in particular completing
 Theorem #85 from https://www.cs.ru.nl/~freek/100/.
 -/
 
+namespace nat
+
 /-- (Impl.) An auxiliary definition for `digits`, to help get the desired definitional unfolding. -/
 def digits_aux_0 : ℕ → list ℕ
 | 0 := []
@@ -541,3 +543,5 @@ begin
   rw of_digits_neg_one at t,
   exact t,
 end
+
+end nat