Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 92c0125

Browse files
chore(data/nat/digits): use nat namespace (#4201)
Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
1 parent 4a8c38e commit 92c0125

File tree

2 files changed

+5
-1
lines changed

2 files changed

+5
-1
lines changed

docs/100.yaml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -293,7 +293,7 @@
293293
title : Divisibility by 3 Rule
294294
author : Scott Morrison
295295
decls :
296-
- three_dvd_iff
296+
- nat.three_dvd_iff
297297
86:
298298
title : Lebesgue Measure and Integration
299299
decl : measure_theory.lintegral

src/data/nat/digits.lean

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,8 @@ We also prove some divisibility tests based on digits, in particular completing
1717
Theorem #85 from https://www.cs.ru.nl/~freek/100/.
1818
-/
1919

20+
namespace nat
21+
2022
/-- (Impl.) An auxiliary definition for `digits`, to help get the desired definitional unfolding. -/
2123
def digits_aux_0 : ℕ → list ℕ
2224
| 0 := []
@@ -541,3 +543,5 @@ begin
541543
rw of_digits_neg_one at t,
542544
exact t,
543545
end
546+
547+
end nat

0 commit comments

Comments
 (0)