# Documentation

Mathlib.Data.Nat.Digits

# Digits of a natural number #

This provides a basic API for extracting the digits of a natural number in a given base, and reconstructing numbers from their digits.

We also prove some divisibility tests based on digits, in particular completing Theorem #85 from https://www.cs.ru.nl/~freek/100/.

A basic norm_digits tactic is also provided for proving goals of the form Nat.digits a b = l where a and b are numerals.

(Impl.) An auxiliary definition for digits, to help get the desired definitional unfolding.

Instances For
def Nat.digitsAux1 (n : ) :

(Impl.) An auxiliary definition for digits, to help get the desired definitional unfolding.

Instances For
def Nat.digitsAux (b : ) (h : 2 b) :

(Impl.) An auxiliary definition for digits, to help get the desired definitional unfolding.

Equations
Instances For
@[simp]
theorem Nat.digitsAux_zero (b : ) (h : 2 b) :
= []
theorem Nat.digitsAux_def (b : ) (h : 2 b) (n : ) (w : 0 < n) :
= n % b :: Nat.digitsAux b h (n / b)
def Nat.digits :

digits b n gives the digits, in little-endian order, of a natural number n in a specified base b.

In any base, we have ofDigits b L = L.foldr (fun x y ↦ x + b * y) 0.

• For any 2 ≤ b, we have l < b for any l ∈ digits b n, and the last digit is not zero. This uniquely specifies the behaviour of digits b.
• For b = 1, we define digits 1 n = List.replicate n 1.
• For b = 0, we define digits 0 n = [n], except digits 0 0 = [].

Note this differs from the existing Nat.to_digits in core, which is used for printing numerals. In particular, Nat.to_digits b 0 = , while digits b 0 = [].

Instances For
@[simp]
theorem Nat.digits_zero (b : ) :
= []
@[simp]
theorem Nat.digits_zero_succ (n : ) :
Nat.digits 0 () = [n + 1]
theorem Nat.digits_zero_succ' {n : } :
n 0 = [n]
@[simp]
theorem Nat.digits_one (n : ) :
=
theorem Nat.digits_one_succ (n : ) :
Nat.digits 1 (n + 1) = 1 ::
@[simp]
Nat.digits (b + 2) (n + 1) = (n + 1) % (b + 2) :: Nat.digits (b + 2) ((n + 1) / (b + 2))
theorem Nat.digits_def' {b : } :
1 < b∀ {n : }, 0 < n = n % b :: Nat.digits b (n / b)
@[simp]
theorem Nat.digits_of_lt (b : ) (x : ) (hx : x 0) (hxb : x < b) :
= [x]
theorem Nat.digits_add (b : ) (h : 1 < b) (x : ) (y : ) (hxb : x < b) (hxy : x 0 y 0) :
Nat.digits b (x + b * y) = x ::
def Nat.ofDigits {α : Type u_1} [] (b : α) :
α

ofDigits b L takes a list L of natural numbers, and interprets them as a number in semiring, as the little-endian digits in base b.

Equations
Instances For
theorem Nat.ofDigits_eq_foldr {α : Type u_1} [] (b : α) (L : ) :
= List.foldr (fun x y => x + b * y) 0 L
theorem Nat.ofDigits_eq_sum_map_with_index_aux (b : ) (l : ) :
List.sum (List.zipWith ((fun i a => a * b ^ i) Nat.succ) () l) = b * List.sum (List.zipWith (fun i a => a * b ^ i) () l)
theorem Nat.ofDigits_eq_sum_mapIdx (b : ) (L : ) :
= List.sum (List.mapIdx (fun i a => a * b ^ i) L)
@[simp]
theorem Nat.ofDigits_singleton {b : } {n : } :
Nat.ofDigits b [n] = n
@[simp]
theorem Nat.ofDigits_one_cons {α : Type u_1} [] (h : ) (L : ) :
Nat.ofDigits 1 (h :: L) = h +
theorem Nat.ofDigits_append {b : } {l1 : } {l2 : } :
Nat.ofDigits b (l1 ++ l2) = Nat.ofDigits b l1 + b ^ * Nat.ofDigits b l2
theorem Nat.coe_ofDigits (α : Type u_1) [] (b : ) (L : ) :
↑() = Nat.ofDigits (b) L
theorem Nat.coe_int_ofDigits (b : ) (L : ) :
↑() = Nat.ofDigits (b) L
theorem Nat.digits_zero_of_eq_zero {b : } (h : b 0) {L : } :
= 0∀ (l : ), l Ll = 0
theorem Nat.digits_ofDigits (b : ) (h : 1 < b) (L : ) (w₁ : ∀ (l : ), l Ll < b) (w₂ : ∀ (h : L []), 0) :
Nat.digits b () = L
theorem Nat.ofDigits_digits (b : ) (n : ) :
theorem Nat.ofDigits_one (L : ) :
=

### Properties #

This section contains various lemmas of properties relating to digits and ofDigits.

theorem Nat.digits_eq_nil_iff_eq_zero {b : } {n : } :
= [] n = 0
theorem Nat.digits_ne_nil_iff_ne_zero {b : } {n : } :
[] n 0
theorem Nat.digits_eq_cons_digits_div {b : } {n : } (h : 1 < b) (w : n 0) :
= n % b :: Nat.digits b (n / b)
theorem Nat.digits_getLast {b : } (m : ) (h : 1 < b) (p : []) (q : Nat.digits b (m / b) []) :
@[simp]
theorem Nat.digits_inj_iff {b : } {n : } {m : } :
= n = m
theorem Nat.digits_len (b : ) (n : ) (hb : 1 < b) (hn : n 0) :
theorem Nat.getLast_digit_ne_zero (b : ) {m : } (hm : m 0) :
List.getLast () (_ : []) 0
theorem Nat.digits_lt_base' {b : } {m : } {d : } :
d Nat.digits (b + 2) md < b + 2

The digits in the base b+2 expansion of n are all less than b+2

theorem Nat.digits_lt_base {b : } {m : } {d : } (hb : 1 < b) (hd : d ) :
d < b

The digits in the base b expansion of n are all less than b, if b ≥ 2

theorem Nat.ofDigits_lt_base_pow_length' {b : } {l : } (hl : ∀ (x : ), x lx < b + 2) :
Nat.ofDigits (b + 2) l < (b + 2) ^

an n-digit number in base b + 2 is less than (b + 2)^n

theorem Nat.ofDigits_lt_base_pow_length {b : } {l : } (hb : 1 < b) (hl : ∀ (x : ), x lx < b) :
< b ^

an n-digit number in base b is less than b^n if b > 1

theorem Nat.lt_base_pow_length_digits' {b : } {m : } :
m < (b + 2) ^ List.length (Nat.digits (b + 2) m)

Any number m is less than (b+2)^(number of digits in the base b + 2 representation of m)

theorem Nat.lt_base_pow_length_digits {b : } {m : } (hb : 1 < b) :
m < b ^ List.length ()

Any number m is less than b^(number of digits in the base b representation of m)

theorem Nat.ofDigits_digits_append_digits {b : } {m : } {n : } :
Nat.ofDigits b ( ++ ) = n + b ^ List.length () * m
theorem Nat.digits_append_digits {b : } {m : } {n : } (hb : 0 < b) :
++ = Nat.digits b (n + b ^ List.length () * m)
theorem Nat.le_digits_len_le (b : ) (n : ) (m : ) (h : n m) :
theorem Nat.ofDigits_monotone {p : } {q : } (L : ) (h : p q) :
theorem Nat.sum_le_ofDigits {p : } (L : ) (h : 1 p) :
theorem Nat.digit_sum_le (p : ) (n : ) :
theorem Nat.pow_length_le_mul_ofDigits {b : } {l : } (hl : l []) (hl2 : List.getLast l hl 0) :
(b + 2) ^ (b + 2) * Nat.ofDigits (b + 2) l
theorem Nat.base_pow_length_digits_le' (b : ) (m : ) (hm : m 0) :
(b + 2) ^ List.length (Nat.digits (b + 2) m) (b + 2) * m

Any non-zero natural number m is greater than (b+2)^((number of digits in the base (b+2) representation of m) - 1)

theorem Nat.base_pow_length_digits_le (b : ) (m : ) (hb : 1 < b) :
m 0b ^ List.length () b * m

Any non-zero natural number m is greater than b^((number of digits in the base b representation of m) - 1)

theorem Nat.ofDigits_div_eq_ofDigits_tail {p : } (hpos : 0 < p) (digits : ) (w₁ : ∀ (l : ), l digitsl < p) :
Nat.ofDigits p digits / p = Nat.ofDigits p (List.tail digits)

Interpreting as a base p number and dividing by p is the same as interpreting the tail.

theorem Nat.ofDigits_div_pow_eq_ofDigits_drop {p : } (i : ) (hpos : 0 < p) (digits : ) (w₁ : ∀ (l : ), l digitsl < p) :
Nat.ofDigits p digits / p ^ i = Nat.ofDigits p (List.drop i digits)

Interpreting as a base p number and dividing by p^i is the same as dropping i.

theorem Nat.self_div_pow_eq_ofDigits_drop {p : } (i : ) (n : ) (h : 2 p) :
n / p ^ i = Nat.ofDigits p (List.drop i ())

Dividing n by p^i is like truncating the first i digits of n in base p.

theorem Nat.sub_one_mul_sum_div_pow_eq_sub_sum_digits {p : } (L : ) {h_nonempty : L []} (h_ne_zero : List.getLast L h_nonempty 0) (h_lt : ∀ (l : ), l Ll < p) :
((p - 1) * Finset.sum () fun i => / p ^ ) = -

### Binary #

theorem Nat.digits_two_eq_bits (n : ) :
= List.map (fun b => bif b then 1 else 0) ()

### Modular Arithmetic #

theorem Nat.dvd_ofDigits_sub_ofDigits {α : Type u_1} [] {a : α} {b : α} {k : α} (h : k a - b) (L : ) :
k -
theorem Nat.ofDigits_modEq' (b : ) (b' : ) (k : ) (h : b b' [MOD k]) (L : ) :
theorem Nat.ofDigits_modEq (b : ) (k : ) (L : ) :
Nat.ofDigits (b % k) L [MOD k]
theorem Nat.ofDigits_mod (b : ) (k : ) (L : ) :
% k = Nat.ofDigits (b % k) L % k
theorem Nat.ofDigits_zmodeq' (b : ) (b' : ) (k : ) (h : b b' [ZMOD k]) (L : ) :
theorem Nat.ofDigits_zmodeq (b : ) (k : ) (L : ) :
Nat.ofDigits (b % k) L [ZMOD k]
theorem Nat.ofDigits_zmod (b : ) (k : ) (L : ) :
% k = Nat.ofDigits (b % k) L % k
theorem Nat.modEq_digits_sum (b : ) (b' : ) (h : b' % b = 1) (n : ) :
theorem Nat.zmodeq_ofDigits_digits (b : ) (b' : ) (c : ) (h : b' c [ZMOD b]) (n : ) :
n Nat.ofDigits c (Nat.digits b' n) [ZMOD b]
theorem Nat.ofDigits_neg_one (L : ) :
Nat.ofDigits (-1) L = List.alternatingSum (List.map (fun n => n) L)

## Divisibility #

theorem Nat.dvd_iff_dvd_digits_sum (b : ) (b' : ) (h : b' % b = 1) (n : ) :
theorem Nat.three_dvd_iff (n : ) :

Divisibility by 3 Rule

theorem Nat.dvd_iff_dvd_ofDigits (b : ) (b' : ) (c : ) (h : b b' - c) (n : ) :
b n b Nat.ofDigits c (Nat.digits b' n)
theorem Nat.eleven_dvd_iff {n : } :
11 n 11 List.alternatingSum (List.map (fun n => n) (Nat.digits 10 n))

### norm_digits tactic #

theorem Nat.NormDigits.digits_succ (b : ) (n : ) (m : ) (r : ) (l : ) (e : r + b * m = n) (hr : r < b) (h : = l 1 < b 0 < m) :
= r :: l 1 < b 0 < n
theorem Nat.NormDigits.digits_one (b : ) (n : ) (n0 : 0 < n) (nb : n < b) :
= [n] 1 < b 0 < n