Mathlib.Data.Nat.Digits

Nat.digitsAux0 definition

: ℕ → List ℕ

Full source

/-- (Impl.) An auxiliary definition for `digits`, to help get the desired definitional unfolding. -/
def digitsAux0 : ℕ → List ℕ
  | 0 => []
  | n + 1 => [n + 1]

Auxiliary function for digits (zero case)

Informal description

The auxiliary function `Nat.digitsAux0` maps a natural number `n` to a list of natural numbers as follows: if `n = 0`, it returns the empty list `[]`; otherwise, for `n + 1`, it returns the singleton list `[n + 1]`.

Nat.digitsAux1 definition

(n : ℕ) : List ℕ

Full source

/-- (Impl.) An auxiliary definition for `digits`, to help get the desired definitional unfolding. -/
def digitsAux1 (n : ℕ) : List ℕ :=
  List.replicate n 1

List of `n` ones

Informal description

The auxiliary function `digitsAux1` takes a natural number `n` and returns a list consisting of `n` copies of the number `1`. This is used as a helper function in the definition of the digits of a natural number.

Nat.digitsAux definition

(b : ℕ) (h : 2 ≤ b) : ℕ → List ℕ

Full source

/-- (Impl.) An auxiliary definition for `digits`, to help get the desired definitional unfolding. -/
def digitsAux (b : ℕ) (h : 2 ≤ b) : ℕ → List ℕ
  | 0 => []
  | n + 1 =>
    ((n + 1) % b) :: digitsAux b h ((n + 1) / b)
decreasing_by exact Nat.div_lt_self (Nat.succ_pos _) h

Auxiliary function for digits in base `b`

Informal description

The auxiliary function `digitsAux` takes a base `b` (with `2 ≤ b`), a natural number `n`, and returns the list of digits of `n` in base `b`, from least significant to most significant. For `n = 0`, it returns the empty list. For `n > 0`, it returns `n % b` followed by the digits of `n / b`.

Nat.digitsAux_zero theorem

(b : ℕ) (h : 2 ≤ b) : digitsAux b h 0 = []

Full source

@[simp]
theorem digitsAux_zero (b : ℕ) (h : 2 ≤ b) : digitsAux b h 0 = [] := by rw [digitsAux]

Base case of digits auxiliary function: $\mathrm{digitsAux}_b(0) = []$

Informal description

For any base $b \geq 2$, the auxiliary digits function evaluated at $n = 0$ returns the empty list, i.e., $\mathrm{digitsAux}_b(0) = []$.

Nat.digitsAux_def theorem

(b : ℕ) (h : 2 ≤ b) (n : ℕ) (w : 0 < n) : digitsAux b h n = (n % b) :: digitsAux b h (n / b)

Full source

theorem digitsAux_def (b : ℕ) (h : 2 ≤ b) (n : ℕ) (w : 0 < n) :
    digitsAux b h n = (n % b) :: digitsAux b h (n / b) := by
  cases n
  · cases w
  · rw [digitsAux]

Recursive Definition of Digits in Base $b$ for Positive Numbers

Informal description

For any base $b \geq 2$ and any positive natural number $n > 0$, the digits of $n$ in base $b$ (computed by the auxiliary function `digitsAux`) satisfy the recursive relation: \[ \text{digitsAux}_b(n) = (n \bmod b) :: \text{digitsAux}_b(\lfloor n/b \rfloor) \] where the digits are listed from least significant to most significant.

Nat.digits definition

: ℕ → ℕ → List ℕ

Full source

/-- `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.toDigits` in core, which is used for printing numerals.
In particular, `Nat.toDigits b 0 = ['0']`, while `digits b 0 = []`.
-/
def digits : ℕ → ℕ → List ℕ
  | 0 => digitsAux0
  | 1 => digitsAux1
  | b + 2 => digitsAux (b + 2) (by norm_num)

Digits of a natural number in base `b`

Informal description

The function `digits b n` returns the digits of a natural number `n` in base `b`, listed in little-endian order (least significant digit first). The behavior is defined as follows: - For base `b ≥ 2`, each digit is less than `b` and the last digit is non-zero (unless `n = 0`). - For base `b = 1`, it returns a list of `n` ones. - For base `b = 0`, it returns `[n]` (except `digits 0 0 = []`). The digits satisfy the property that `ofDigits b L = L.foldr (fun x y ↦ x + b * y) 0`, where `ofDigits` reconstructs the number from its digits.

Nat.digits_zero theorem

(b : ℕ) : digits b 0 = []

Full source

@[simp]
theorem digits_zero (b : ℕ) : digits b 0 = [] := by
  rcases b with (_ | ⟨_ | ⟨_⟩⟩) <;> simp [digits, digitsAux0, digitsAux1]

Digits of Zero in Any Base is Empty List

Informal description

For any natural number base $b$, the digits of $0$ in base $b$ form the empty list, i.e., $\mathrm{digits}(b, 0) = []$.

Nat.digits_zero_zero theorem

: digits 0 0 = []

Full source

theorem digits_zero_zero : digits 0 0 = [] :=
  rfl

Digits of Zero in Base Zero is Empty List

Informal description

The digits of the number $0$ in base $0$ is the empty list, i.e., $\mathrm{digits}(0, 0) = []$.

Nat.digits_zero_succ theorem

(n : ℕ) : digits 0 n.succ = [n + 1]

Full source

@[simp]
theorem digits_zero_succ (n : ℕ) : digits 0 n.succ = [n + 1] :=
  rfl

Digits of Successor in Base Zero

Informal description

For any natural number $n$, the digits of $n+1$ in base $0$ is the singleton list $[n+1]$, i.e., $\mathrm{digits}(0, n+1) = [n+1]$.

Nat.digits_zero_succ' theorem

: ∀ {n : ℕ}, n ≠ 0 → digits 0 n = [n]

Full source

theorem digits_zero_succ' : ∀ {n : ℕ}, n ≠ 0 → digits 0 n = [n]
  | 0, h => (h rfl).elim
  | _ + 1, _ => rfl

Digits of Nonzero Number in Base Zero is Singleton List

Informal description

For any nonzero natural number $n$, the digits of $n$ in base $0$ is the singleton list $[n]$, i.e., $\mathrm{digits}(0, n) = [n]$.

Nat.digits_one theorem

(n : ℕ) : digits 1 n = List.replicate n 1

Full source

@[simp]
theorem digits_one (n : ℕ) : digits 1 n = List.replicate n 1 :=
  rfl

Digits in Base One: $\mathrm{digits}(1, n) = [1, \ldots, 1]$ (length $n$)

Informal description

For any natural number $n$, the digits of $n$ in base $1$ are given by a list of $n$ ones, i.e., $\mathrm{digits}(1, n) = [1, \ldots, 1]$ (with $n$ elements).

Nat.digits_one_succ theorem

(n : ℕ) : digits 1 (n + 1) = 1 :: digits 1 n

Full source

theorem digits_one_succ (n : ℕ) : digits 1 (n + 1) = 1 :: digits 1 n :=
  rfl

Recursive digit construction in base 1: $\mathrm{digits}_1(n+1) = 1 :: \mathrm{digits}_1(n)$

Informal description

For any natural number $n$, the digits of $n+1$ in base $1$ are obtained by prepending $1$ to the digits of $n$ in base $1$, i.e., $\mathrm{digits}_1(n+1) = 1 :: \mathrm{digits}_1(n)$.

Nat.digits_add_two_add_one theorem

(b n : ℕ) : digits (b + 2) (n + 1) = ((n + 1) % (b + 2)) :: digits (b + 2) ((n + 1) / (b + 2))

Full source

theorem digits_add_two_add_one (b n : ℕ) :
    digits (b + 2) (n + 1) = ((n + 1) % (b + 2)) :: digits (b + 2) ((n + 1) / (b + 2)) := by
  simp [digits, digitsAux_def]

Recursive digit construction in base $b + 2$: $\mathrm{digits}_{b+2}(n + 1) = (n + 1 \bmod b + 2) :: \mathrm{digits}_{b+2}(\lfloor (n + 1)/(b + 2) \rfloor)$

Informal description

For any natural numbers $b$ and $n$, the digits of $n + 1$ in base $b + 2$ are given by $(n + 1) \bmod (b + 2)$ followed by the digits of $\lfloor (n + 1) / (b + 2) \rfloor$ in the same base. That is, \[ \mathrm{digits}_{b+2}(n + 1) = \big((n + 1) \bmod (b + 2)\big) :: \mathrm{digits}_{b+2}\left(\left\lfloor \frac{n + 1}{b + 2} \right\rfloor\right). \]

Nat.digits_of_two_le_of_pos theorem

{b : ℕ} (hb : 2 ≤ b) (hn : 0 < n) : Nat.digits b n = n % b :: Nat.digits b (n / b)

Full source

@[simp]
lemma digits_of_two_le_of_pos {b : ℕ} (hb : 2 ≤ b) (hn : 0 < n) :
    Nat.digits b n = n % b :: Nat.digits b (n / b) := by
  rw [Nat.eq_add_of_sub_eq hb rfl, Nat.eq_add_of_sub_eq hn rfl, Nat.digits_add_two_add_one]

Recursive Digit Construction in Base $b \geq 2$ for Positive Numbers

Informal description

For any natural numbers $b$ and $n$ such that $b \geq 2$ and $n > 0$, the digits of $n$ in base $b$ are given by the least significant digit $n \bmod b$ followed by the digits of $\lfloor n/b \rfloor$ in the same base. That is, \[ \mathrm{digits}_b(n) = (n \bmod b) :: \mathrm{digits}_b\left(\left\lfloor \frac{n}{b} \right\rfloor\right). \]

Nat.digits_def' theorem

: ∀ {b : ℕ} (_ : 1 < b) {n : ℕ} (_ : 0 < n), digits b n = (n % b) :: digits b (n / b)

Full source

theorem digits_def' :
    ∀ {b : ℕ} (_ : 1 < b) {n : ℕ} (_ : 0 < n), digits b n = (n % b) :: digits b (n / b)
  | 0, h => absurd h (by decide)
  | 1, h => absurd h (by decide)
  | b + 2, _ => digitsAux_def _ (by simp) _

Recursive Definition of Digits in Base $b$ for Positive Numbers

Informal description

For any base $b > 1$ and any positive natural number $n > 0$, the digits of $n$ in base $b$ satisfy the recursive relation: \[ \text{digits}_b(n) = (n \bmod b) :: \text{digits}_b(\lfloor n/b \rfloor) \] where the digits are listed from least significant to most significant.

Nat.digits_of_lt theorem

(b x : ℕ) (hx : x ≠ 0) (hxb : x < b) : digits b x = [x]

Full source

@[simp]
theorem digits_of_lt (b x : ℕ) (hx : x ≠ 0) (hxb : x < b) : digits b x = [x] := by
  rcases exists_eq_succ_of_ne_zero hx with ⟨x, rfl⟩
  rcases Nat.exists_eq_add_of_le' ((Nat.le_add_left 1 x).trans_lt hxb) with ⟨b, rfl⟩
  rw [digits_add_two_add_one, div_eq_of_lt hxb, digits_zero, mod_eq_of_lt hxb]

Single-digit representation of $x$ in base $b$ when $0 < x < b$

Informal description

For any natural numbers $b$ and $x$ where $x$ is nonzero ($x \neq 0$) and $x$ is less than $b$ ($x < b$), the digits of $x$ in base $b$ consist of the single-element list $[x]$.

Nat.digits_add theorem

(b : ℕ) (h : 1 < b) (x y : ℕ) (hxb : x < b) (hxy : x ≠ 0 ∨ y ≠ 0) : digits b (x + b * y) = x :: digits b y

Full source

theorem digits_add (b : ℕ) (h : 1 < b) (x y : ℕ) (hxb : x < b) (hxy : x ≠ 0x ≠ 0 ∨ y ≠ 0) :
    digits b (x + b * y) = x :: digits b y := by
  rcases Nat.exists_eq_add_of_le' h with ⟨b, rfl : _ = _ + 2⟩
  cases y
  · simp [hxb, hxy.resolve_right (absurd rfl)]
  dsimp [digits]
  rw [digitsAux_def]
  · congr
    · simp [Nat.add_mod, mod_eq_of_lt hxb]
    · simp [add_mul_div_left, div_eq_of_lt hxb]
  · apply Nat.succ_pos

Digit expansion of $x + b \cdot y$ in base $b > 1$ when $x < b$ and $x$ or $y$ is nonzero

Informal description

For any natural numbers $b > 1$, $x < b$, and $y$ such that either $x \neq 0$ or $y \neq 0$, the digits of $x + b \cdot y$ in base $b$ are given by $x$ followed by the digits of $y$ in base $b$, i.e., \[ \mathrm{digits}_b(x + b \cdot y) = x :: \mathrm{digits}_b(y). \]

Nat.ofDigits definition

{α : Type*} [Semiring α] (b : α) : List ℕ → α

Full source

/-- `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`.
-/
def ofDigits {α : Type*} [Semiring α] (b : α) : List ℕ → α
  | [] => 0
  | h :: t => h + b * ofDigits b t

Interpretation of digits in a given base as a number

Informal description

Given a base $b$ in a semiring $\alpha$ and a list $L$ of natural numbers, the function $\text{ofDigits}$ interprets $L$ as a number in $\alpha$ by treating the list as little-endian digits in base $b$. Specifically, it recursively computes the value as $h + b \cdot \text{ofDigits } b \text{ } t$ for a list with head $h$ and tail $t$, and returns $0$ for an empty list.

Nat.ofDigits_eq_foldr theorem

{α : Type*} [Semiring α] (b : α) (L : List ℕ) : ofDigits b L = List.foldr (fun x y => ↑x + b * y) 0 L

Full source

theorem ofDigits_eq_foldr {α : Type*} [Semiring α] (b : α) (L : List ℕ) :
    ofDigits b L = List.foldr (fun x y => ↑x + b * y) 0 L := by
  induction' L with d L ih
  · rfl
  · dsimp [ofDigits]
    rw [ih]

Digit Expansion as Right Fold: $\text{ofDigits}_b(L) = \text{foldr}\,(\lambda x y \mapsto x + b \cdot y)\,0\,L$

Informal description

For any semiring $\alpha$, base $b \in \alpha$, and list of natural numbers $L$, the value $\text{ofDigits}_b(L)$ obtained by interpreting $L$ as digits in base $b$ equals the right fold of $L$ with the operation $\lambda x y \mapsto x + b \cdot y$ starting from $0$.

Nat.ofDigits_eq_sum_mapIdx_aux theorem

 (b : ℕ) (l : List ℕ) :
  (l.zipWith ((fun a i : ℕ => a * b ^ (i + 1))) (List.range l.length)).sum =
    b * (l.zipWith (fun a i => a * b ^ i) (List.range l.length)).sum

Full source

theorem ofDigits_eq_sum_mapIdx_aux (b : ℕ) (l : List ℕ) :
    (l.zipWith ((fun a i : ℕ => a * b ^ (i + 1))) (List.range l.length)).sum =
      b * (l.zipWith (fun a i => a * b ^ i) (List.range l.length)).sum := by
  suffices
    l.zipWith (fun a i : ℕ => a * b ^ (i + 1)) (List.range l.length) =
      l.zipWith (fun a i=> b * (a * b ^ i)) (List.range l.length)
    by simp [this]
  congr; ext; simp [pow_succ]; ring

Auxiliary Summation Identity for Digit Expansion Coefficients

Informal description

For any natural number $b$ and list of natural numbers $l$, the sum of the list obtained by zipping $l$ with the function $(a, i) \mapsto a \cdot b^{i+1}$ (where $i$ ranges over the indices of $l$) equals $b$ times the sum of the list obtained by zipping $l$ with the function $(a, i) \mapsto a \cdot b^i$.

Nat.ofDigits_eq_sum_mapIdx theorem

(b : ℕ) (L : List ℕ) : ofDigits b L = (L.mapIdx fun i a => a * b ^ i).sum

Full source

theorem ofDigits_eq_sum_mapIdx (b : ℕ) (L : List ℕ) :
    ofDigits b L = (L.mapIdx fun i a => a * b ^ i).sum := by
  rw [List.mapIdx_eq_zipIdx_map, List.zipIdx_eq_zip_range', List.map_zip_eq_zipWith,
    ofDigits_eq_foldr, ← List.range_eq_range']
  induction' L with hd tl hl
  · simp
  · simpa [List.range_succ_eq_map, List.zipWith_map_right, ofDigits_eq_sum_mapIdx_aux] using
      Or.inl hl

Digit Expansion as Sum of Scaled Powers: $\text{ofDigits}_b(L) = \sum_i L_i b^i$

Informal description

For any natural number base $b$ and list of natural numbers $L$, the value obtained by interpreting $L$ as digits in base $b$ equals the sum of each digit multiplied by $b$ raised to its position index, i.e., $$\text{ofDigits}_b(L) = \sum_{i} L_i \cdot b^i$$ where $L_i$ denotes the digit at position $i$ in $L$ (with $i$ starting from 0).

Nat.ofDigits_nil theorem

{b : ℕ} : ofDigits b [] = 0

Full source

@[simp]
theorem ofDigits_nil {b : ℕ} : ofDigits b [] = 0 := rfl

Empty Digit List Yields Zero in Any Base

Informal description

For any natural number base $b$, interpreting an empty list of digits in base $b$ yields the number $0$, i.e., $\text{ofDigits}(b, []) = 0$.

Nat.ofDigits_singleton theorem

{b n : ℕ} : ofDigits b [n] = n

Full source

@[simp]
theorem ofDigits_singleton {b n : ℕ} : ofDigits b [n] = n := by simp [ofDigits]

Singleton Digit List Yields the Digit Itself

Informal description

For any natural numbers $b$ and $n$, interpreting the singleton list $[n]$ as a digit in base $b$ yields $n$, i.e., $\text{ofDigits}(b, [n]) = n$.

Nat.ofDigits_one_cons theorem

{α : Type*} [Semiring α] (h : ℕ) (L : List ℕ) : ofDigits (1 : α) (h :: L) = h + ofDigits 1 L

Full source

@[simp]
theorem ofDigits_one_cons {α : Type*} [Semiring α] (h : ℕ) (L : List ℕ) :
    ofDigits (1 : α) (h :: L) = h + ofDigits 1 L := by simp [ofDigits]

Recursive Digit Interpretation in Base 1

Informal description

For any semiring $\alpha$, natural number $h$, and list of natural numbers $L$, interpreting the list $h :: L$ as digits in base $1$ yields $h$ plus the interpretation of $L$ in base $1$, i.e., $$\text{ofDigits}_1(h :: L) = h + \text{ofDigits}_1(L).$$

Nat.ofDigits_cons theorem

{b hd} {tl : List ℕ} : ofDigits b (hd :: tl) = hd + b * ofDigits b tl

Full source

theorem ofDigits_cons {b hd} {tl : List ℕ} :
    ofDigits b (hd :: tl) = hd + b * ofDigits b tl := rfl

Recursive Digit Interpretation in Base $b$

Informal description

For any natural number base $b$, head digit $hd$, and tail list of digits $tl$, the value of the digits list $hd :: tl$ interpreted in base $b$ is equal to $hd$ plus $b$ multiplied by the value of the tail digits $tl$ interpreted in base $b$, i.e., $$\text{ofDigits}_b(hd :: tl) = hd + b \cdot \text{ofDigits}_b(tl).$$

Nat.ofDigits_append theorem

{b : ℕ} {l1 l2 : List ℕ} : ofDigits b (l1 ++ l2) = ofDigits b l1 + b ^ l1.length * ofDigits b l2

Full source

theorem ofDigits_append {b : ℕ} {l1 l2 : List ℕ} :
    ofDigits b (l1 ++ l2) = ofDigits b l1 + b ^ l1.length * ofDigits b l2 := by
  induction' l1 with hd tl IH
  · simp [ofDigits]
  · rw [ofDigits, List.cons_append, ofDigits, IH, List.length_cons, pow_succ']
    ring

Concatenation Property of Digit Interpretation in Base $b$

Informal description

For any natural number base $b$ and two lists of natural numbers $l_1$ and $l_2$, the value of the concatenated list $l_1 ++ l_2$ interpreted as digits in base $b$ equals the value of $l_1$ plus $b$ raised to the power of the length of $l_1$ multiplied by the value of $l_2$, i.e., $$\text{ofDigits}_b(l_1 \mathbin{+\kern-1.5ex+} l_2) = \text{ofDigits}_b(l_1) + b^{|l_1|} \cdot \text{ofDigits}_b(l_2).$$

Nat.coe_ofDigits theorem

(α : Type*) [Semiring α] (b : ℕ) (L : List ℕ) : ((ofDigits b L : ℕ) : α) = ofDigits (b : α) L

Full source

@[norm_cast]
theorem coe_ofDigits (α : Type*) [Semiring α] (b : ℕ) (L : List ℕ) :
    ((ofDigits b L : ℕ) : α) = ofDigits (b : α) L := by
  induction' L with d L ih
  · simp [ofDigits]
  · dsimp [ofDigits]; push_cast; rw [ih]

Canonical Homomorphism Commutes with Digit Interpretation: $\text{cast}(\text{ofDigits}_b(L)) = \text{ofDigits}_{\text{cast}(b)}(L)$

Informal description

Let $\alpha$ be a semiring and $b$ be a natural number. For any list of natural numbers $L$, the canonical homomorphism from $\mathbb{N}$ to $\alpha$ applied to the number represented by $L$ in base $b$ equals the number represented by $L$ in base $b$ (viewed as an element of $\alpha$). That is, $$ \text{cast}(\text{ofDigits}_b(L)) = \text{ofDigits}_{\text{cast}(b)}(L). $$

Nat.coe_int_ofDigits theorem

(b : ℕ) (L : List ℕ) : ((ofDigits b L : ℕ) : ℤ) = ofDigits (b : ℤ) L

Full source

@[norm_cast]
theorem coe_int_ofDigits (b : ℕ) (L : List ℕ) : ((ofDigits b L : ℕ) : ℤ) = ofDigits (b : ℤ) L := by
  induction' L with d L _
  · rfl
  · dsimp [ofDigits]; push_cast; simp only

Canonical Homomorphism Commutes with Digit Interpretation in Integers: $\text{cast}(\text{ofDigits}_b(L)) = \text{ofDigits}_{\text{cast}(b)}(L)$

Informal description

For any natural number base $b$ and list of natural numbers $L$, the canonical homomorphism from $\mathbb{N}$ to $\mathbb{Z}$ applied to the number represented by $L$ in base $b$ equals the number represented by $L$ in base $b$ (viewed as an integer). That is, $$ \text{cast}(\text{ofDigits}_b(L)) = \text{ofDigits}_{\text{cast}(b)}(L). $$

Nat.digits_zero_of_eq_zero theorem

{b : ℕ} (h : b ≠ 0) : ∀ {L : List ℕ} (_ : ofDigits b L = 0), ∀ l ∈ L, l = 0

Full source

theorem digits_zero_of_eq_zero {b : ℕ} (h : b ≠ 0) :
    ∀ {L : List ℕ} (_ : ofDigits b L = 0), ∀ l ∈ L, l = 0
  | _ :: _, h0, _, List.Mem.headList.Mem.head .. => Nat.eq_zero_of_add_eq_zero_right h0
  | _ :: _, h0, _, List.Mem.tailList.Mem.tail _ hL =>
    digits_zero_of_eq_zero h (mul_right_injective₀ h (Nat.eq_zero_of_add_eq_zero_left h0)) _ hL

All Digits Zero When Number is Zero in Base $b$

Informal description

For any natural number base $b \neq 0$ and any list of digits $L$ interpreted in base $b$, if the value of $L$ in base $b$ is zero (i.e., $\text{ofDigits}(b, L) = 0$), then every digit $l$ in $L$ must be zero.

Nat.digits_ofDigits theorem

 (b : ℕ) (h : 1 < b) (L : List ℕ) (w₁ : ∀ l ∈ L, l < b) (w₂ : ∀ h : L ≠ [], L.getLast h ≠ 0) :
  digits b (ofDigits b L) = L

Full source

theorem digits_ofDigits (b : ℕ) (h : 1 < b) (L : List ℕ) (w₁ : ∀ l ∈ L, l < b)
    (w₂ : ∀ h : L ≠ [], L.getLast h ≠ 0) : digits b (ofDigits b L) = L := by
  induction' L with d L ih
  · dsimp [ofDigits]
    simp
  · dsimp [ofDigits]
    replace w₂ := w₂ (by simp)
    rw [digits_add b h]
    · rw [ih]
      · intro l m
        apply w₁
        exact List.mem_cons_of_mem _ m
      · intro h
        rw [List.getLast_cons h] at w₂
        convert w₂
    · exact w₁ d List.mem_cons_self
    · by_cases h' : L = []
      · rcases h' with rfl
        left
        simpa using w₂
      · right
        contrapose! w₂
        refine digits_zero_of_eq_zero h.ne_bot w₂ _ ?_
        rw [List.getLast_cons h']
        exact List.getLast_mem h'

Digits of Reconstructed Number in Base $b > 1$

Informal description

For any natural number base $b > 1$ and any list of digits $L$ in base $b$ (where each digit $l \in L$ satisfies $l < b$ and the last digit is non-zero if $L$ is non-empty), the digits of the number reconstructed from $L$ in base $b$ are exactly $L$, i.e., $$\mathrm{digits}_b(\mathrm{ofDigits}_b(L)) = L.$$

Nat.ofDigits_digits theorem

(b n : ℕ) : ofDigits b (digits b n) = n

Full source

theorem ofDigits_digits (b n : ℕ) : ofDigits b (digits b n) = n := by
  rcases b with - | b
  · rcases n with - | n
    · rfl
    · simp
  · rcases b with - | b
    · induction' n with n ih
      · rfl
      · rw [Nat.zero_add] at ih ⊢
        simp only [ih, add_comm 1, ofDigits_one_cons, Nat.cast_id, digits_one_succ]
    · induction n using Nat.strongRecOn with | ind n h => ?_
      cases n
      · rw [digits_zero]
        rfl
      · simp only [Nat.succ_eq_add_one, digits_add_two_add_one]
        dsimp [ofDigits]
        rw [h _ (Nat.div_lt_self' _ b)]
        rw [Nat.mod_add_div]

Reconstruction of Number from Its Digits in Base $b$

Informal description

For any natural numbers $b$ and $n$, the number reconstructed from its digits in base $b$ equals $n$, i.e., $$\text{ofDigits}_b(\text{digits}_b(n)) = n.$$

Nat.ofDigits_one theorem

(L : List ℕ) : ofDigits 1 L = L.sum

Full source

theorem ofDigits_one (L : List ℕ) : ofDigits 1 L = L.sum := by
  induction L with
  | nil => rfl
  | cons _ _ ih => simp [ofDigits, List.sum_cons, ih]

Base-1 Digits Sum Identity

Informal description

For any list of natural numbers $L$, interpreting $L$ as digits in base $1$ via the `ofDigits` function yields the sum of the elements of $L$, i.e., $\text{ofDigits } 1 \text{ } L = \sum L$.

Nat.digits_eq_nil_iff_eq_zero theorem

{b n : ℕ} : digits b n = [] ↔ n = 0

Full source

theorem digits_eq_nil_iff_eq_zero {b n : ℕ} : digitsdigits b n = [] ↔ n = 0 := by
  constructor
  · intro h
    have : ofDigits b (digits b n) = ofDigits b [] := by rw [h]
    convert this
    rw [ofDigits_digits]
  · rintro rfl
    simp

Empty Digits List Characterizes Zero

Informal description

For any natural numbers $b$ and $n$, the digits of $n$ in base $b$ form the empty list if and only if $n = 0$. That is, $$\mathrm{digits}_b(n) = [] \leftrightarrow n = 0.$$

Nat.digits_ne_nil_iff_ne_zero theorem

{b n : ℕ} : digits b n ≠ [] ↔ n ≠ 0

Full source

theorem digits_ne_nil_iff_ne_zero {b n : ℕ} : digitsdigits b n ≠ []digits b n ≠ [] ↔ n ≠ 0 :=
  not_congr digits_eq_nil_iff_eq_zero

Non-Empty Digits List Characterizes Non-Zero Number

Informal description

For any natural numbers $b$ and $n$, the digits of $n$ in base $b$ form a non-empty list if and only if $n \neq 0$. That is, $$\mathrm{digits}_b(n) \neq [] \leftrightarrow n \neq 0.$$

Nat.digits_eq_cons_digits_div theorem

{b n : ℕ} (h : 1 < b) (w : n ≠ 0) : digits b n = (n % b) :: digits b (n / b)

Full source

theorem digits_eq_cons_digits_div {b n : ℕ} (h : 1 < b) (w : n ≠ 0) :
    digits b n = (n % b) :: digits b (n / b) := by
  rcases b with (_ | _ | b)
  · rw [digits_zero_succ' w, Nat.mod_zero, Nat.div_zero, Nat.digits_zero_zero]
  · norm_num at h
  rcases n with (_ | n)
  · norm_num at w
  · simp only [digits_add_two_add_one, ne_eq]

Recursive digit decomposition in base $b > 1$: $\mathrm{digits}_b(n) = (n \bmod b) :: \mathrm{digits}_b(\lfloor n/b \rfloor)$ for $n \neq 0$

Informal description

For any natural numbers $b > 1$ and $n \neq 0$, the digits of $n$ in base $b$ are given by the remainder $n \bmod b$ followed by the digits of $\lfloor n / b \rfloor$ in base $b$. That is, \[ \mathrm{digits}_b(n) = (n \bmod b) :: \mathrm{digits}_b\left(\left\lfloor \frac{n}{b} \right\rfloor\right). \]

Nat.digits_getLast theorem

{b : ℕ} (m : ℕ) (h : 1 < b) (p q) : (digits b m).getLast p = (digits b (m / b)).getLast q

Full source

theorem digits_getLast {b : ℕ} (m : ℕ) (h : 1 < b) (p q) :
    (digits b m).getLast p = (digits b (m / b)).getLast q := by
  by_cases hm : m = 0
  · simp [hm]
  simp only [digits_eq_cons_digits_div h hm]
  rw [List.getLast_cons]

Last Digit Invariance Under Division by Base: $\mathrm{getLast}(\mathrm{digits}_b(m)) = \mathrm{getLast}(\mathrm{digits}_b(\lfloor m / b \rfloor))$ for $b > 1$

Informal description

For any natural numbers $b > 1$ and $m$, the last digit of $m$ in base $b$ is equal to the last digit of $\lfloor m / b \rfloor$ in base $b$. That is, if $L = \mathrm{digits}_b(m)$ and $L' = \mathrm{digits}_b(\lfloor m / b \rfloor)$, then $\mathrm{getLast}(L) = \mathrm{getLast}(L')$ for any proofs $p$ and $q$ that $L$ and $L'$ are non-empty.

Nat.digits.injective theorem

(b : ℕ) : Function.Injective b.digits

Full source

theorem digits.injective (b : ℕ) : Function.Injective b.digits :=
  Function.LeftInverse.injective (ofDigits_digits b)

Injectivity of the digit function in base $b$

Informal description

For any natural number $b$, the function $\mathrm{digits}_b : \mathbb{N} \to \mathrm{List}\ \mathbb{N}$ that maps a natural number to its digits in base $b$ is injective. That is, for any $n, m \in \mathbb{N}$, if $\mathrm{digits}_b(n) = \mathrm{digits}_b(m)$, then $n = m$.

Nat.digits_inj_iff theorem

{b n m : ℕ} : b.digits n = b.digits m ↔ n = m

Full source

@[simp]
theorem digits_inj_iff {b n m : ℕ} : b.digits n = b.digits m ↔ n = m :=
  (digits.injective b).eq_iff

Equality of Natural Numbers via Digit Equality: $\mathrm{digits}_b(n) = \mathrm{digits}_b(m) \leftrightarrow n = m$

Informal description

For any natural numbers $b$, $n$, and $m$, the digits of $n$ in base $b$ are equal to the digits of $m$ in base $b$ if and only if $n = m$.

Nat.digits_len theorem

(b n : ℕ) (hb : 1 < b) (hn : n ≠ 0) : (b.digits n).length = b.log n + 1

Full source

theorem digits_len (b n : ℕ) (hb : 1 < b) (hn : n ≠ 0) : (b.digits n).length = b.log n + 1 := by
  induction' n using Nat.strong_induction_on with n IH
  rw [digits_eq_cons_digits_div hb hn, List.length]
  by_cases h : n / b = 0
  · simp [IH, h]
    aesop
  · have : n / b < n := div_lt_self (Nat.pos_of_ne_zero hn) hb
    rw [IH _ this h, log_div_base, tsub_add_cancel_of_le]
    refine Nat.succ_le_of_lt (log_pos hb ?_)
    contrapose! h
    exact div_eq_of_lt h

Length of Digits Formula: $\mathrm{length}(\mathrm{digits}_b(n)) = \log_b n + 1$ for $b > 1$ and $n \neq 0$

Informal description

For any natural numbers $b > 1$ and $n \neq 0$, the length of the digits of $n$ in base $b$ is equal to $\log_b n + 1$, where $\log_b n$ is the floor logarithm of $n$ in base $b$.

Nat.getLast_digit_ne_zero theorem

(b : ℕ) {m : ℕ} (hm : m ≠ 0) : (digits b m).getLast (digits_ne_nil_iff_ne_zero.mpr hm) ≠ 0

Full source

theorem getLast_digit_ne_zero (b : ℕ) {m : ℕ} (hm : m ≠ 0) :
    (digits b m).getLast (digits_ne_nil_iff_ne_zero.mpr hm) ≠ 0 := by
  rcases b with (_ | _ | b)
  · cases m
    · cases hm rfl
    · simp
  · cases m
    · cases hm rfl
    rename ℕ => m
    simp only [zero_add, digits_one, List.getLast_replicate_succ m 1]
    exact Nat.one_ne_zero
  revert hm
  induction m using Nat.strongRecOn with | ind n IH => ?_
  intro hn
  by_cases hnb : n < b + 2
  · simpa only [digits_of_lt (b + 2) n hn hnb]
  · rw [digits_getLast n (le_add_left 2 b)]
    refine IH _ (Nat.div_lt_self hn.bot_lt (one_lt_succ_succ b)) ?_
    rw [← pos_iff_ne_zero]
    exact Nat.div_pos (le_of_not_lt hnb) (zero_lt_succ (succ b))

Non-Zero Last Digit Property for Natural Numbers in Base $b$

Informal description

For any natural numbers $b$ and $m$ with $m \neq 0$, the last digit of $m$ in base $b$ is non-zero. That is, if $L = \mathrm{digits}_b(m)$, then $\mathrm{getLast}(L) \neq 0$.

Nat.mul_ofDigits theorem

(n : ℕ) {b : ℕ} {l : List ℕ} : n * ofDigits b l = ofDigits b (l.map (n * ·))

Full source

theorem mul_ofDigits (n : ℕ) {b : ℕ} {l : List ℕ} :
    n * ofDigits b l = ofDigits b (l.map (n * ·)) := by
  induction l with
  | nil => rfl
  | cons hd tl ih =>
    rw [List.map_cons, ofDigits_cons, ofDigits_cons, ← ih]
    ring

Multiplication of Number by Scalar Preserves Digit Interpretation in Base $b$

Informal description

For any natural number $n$, base $b$, and list of digits $l$, the product of $n$ with the number represented by digits $l$ in base $b$ is equal to the number represented by the list obtained by multiplying each digit in $l$ by $n$, interpreted in the same base $b$. That is, $$n \cdot \text{ofDigits}_b(l) = \text{ofDigits}_b(l \text{ map } (n \cdot \cdot)).$$

Nat.ofDigits_inj_of_len_eq theorem

 {b : ℕ} (hb : 1 < b) {L1 L2 : List ℕ} (len : L1.length = L2.length) (w1 : ∀ l ∈ L1, l < b) (w2 : ∀ l ∈ L2, l < b)
  (h : ofDigits b L1 = ofDigits b L2) : L1 = L2

Full source

lemma ofDigits_inj_of_len_eq {b : ℕ} (hb : 1 < b) {L1 L2 : List ℕ}
    (len : L1.length = L2.length) (w1 : ∀ l ∈ L1, l < b) (w2 : ∀ l ∈ L2, l < b)
    (h : ofDigits b L1 = ofDigits b L2) : L1 = L2 := by
  induction' L1 with D L ih generalizing L2
  · simp only [List.length_nil] at len
    exact (List.length_eq_zero_iff.mp len.symm).symm
  obtain ⟨d, l, rfl⟩ := List.exists_cons_of_length_eq_add_one len.symm
  simp only [List.length_cons, add_left_inj] at len
  simp only [ofDigits_cons] at h
  have eqd : D = d := by
    have H : (D + b * ofDigits b L) % b = (d + b * ofDigits b l) % b := by rw [h]
    simpa [mod_eq_of_lt (w2 d List.mem_cons_self),
      mod_eq_of_lt (w1 D List.mem_cons_self)] using H
  simp only [eqd, add_right_inj, mul_left_cancel_iff_of_pos (zero_lt_of_lt hb)] at h
  have := ih len (fun a ha ↦ w1 a <| List.mem_cons_of_mem D ha)
    (fun a ha ↦ w2 a <| List.mem_cons_of_mem d ha) h
  rw [eqd, this]

Injectivity of Digit Interpretation for Equal-Length Lists in Base $b > 1$

Informal description

Let $b$ be a natural number greater than $1$, and let $L_1$ and $L_2$ be two lists of natural numbers of equal length. If every digit in $L_1$ is less than $b$, every digit in $L_2$ is less than $b$, and the numbers represented by $L_1$ and $L_2$ in base $b$ are equal, then $L_1$ and $L_2$ are identical lists.

Nat.ofDigits_add_ofDigits_eq_ofDigits_zipWith_of_length_eq theorem

 {b : ℕ} {l1 l2 : List ℕ} (h : l1.length = l2.length) :
  ofDigits b l1 + ofDigits b l2 = ofDigits b (l1.zipWith (· + ·) l2)

Full source

/-- The addition of ofDigits of two lists is equal to ofDigits of digit-wise addition of them -/
theorem ofDigits_add_ofDigits_eq_ofDigits_zipWith_of_length_eq {b : ℕ} {l1 l2 : List ℕ}
    (h : l1.length = l2.length) :
    ofDigits b l1 + ofDigits b l2 = ofDigits b (l1.zipWith (· + ·) l2) := by
  induction l1 generalizing l2 with
  | nil => simp_all [eq_comm, List.length_eq_zero_iff, ofDigits]
  | cons hd₁ tl₁ ih₁ =>
    induction l2 generalizing tl₁ with
    | nil => simp_all
    | cons hd₂ tl₂ ih₂ =>
      simp_all only [List.length_cons, succ_eq_add_one, ofDigits_cons, add_left_inj,
        eq_comm, List.zipWith_cons_cons, add_eq]
      rw [← ih₁ h.symm, mul_add]
      ac_rfl

Digit-wise Addition Preserves Base Interpretation for Equal-Length Digit Lists

Informal description

For any base $b \in \mathbb{N}$ and two lists of digits $l_1$ and $l_2$ of equal length, the sum of the numbers represented by $l_1$ and $l_2$ in base $b$ is equal to the number represented by the list obtained from digit-wise addition of $l_1$ and $l_2$ in base $b$. That is, $$\text{ofDigits}_b(l_1) + \text{ofDigits}_b(l_2) = \text{ofDigits}_b(\text{zipWith } (+) l_1 l_2).$$

Nat.digits_lt_base' theorem

{b m : ℕ} : ∀ {d}, d ∈ digits (b + 2) m → d < b + 2

Full source

/-- The digits in the base b+2 expansion of n are all less than b+2 -/
theorem digits_lt_base' {b m : ℕ} : ∀ {d}, d ∈ digits (b + 2) m → d < b + 2 := by
  induction m using Nat.strongRecOn with | ind n IH => ?_
  intro d hd
  rcases n with - | n
  · rw [digits_zero] at hd
    cases hd
  -- base b+2 expansion of 0 has no digits
  rw [digits_add_two_add_one] at hd
  cases hd
  · exact n.succ.mod_lt (by linarith)
  · apply IH ((n + 1) / (b + 2))
    · apply Nat.div_lt_self <;> omega
    · assumption

Digits in Base $b+2$ are Bounded by $b+2$

Informal description

For any natural numbers $b$ and $m$, every digit $d$ in the base $b+2$ expansion of $m$ satisfies $d < b+2$.

Nat.digits_lt_base theorem

{b m d : ℕ} (hb : 1 < b) (hd : d ∈ digits b m) : d < b

Full source

/-- The digits in the base b expansion of n are all less than b, if b ≥ 2 -/
theorem digits_lt_base {b m d : ℕ} (hb : 1 < b) (hd : d ∈ digits b m) : d < b := by
  rcases b with (_ | _ | b) <;> try simp_all
  exact digits_lt_base' hd

Digits in Base $b$ are Bounded by $b$ for $b \geq 2$

Informal description

For any natural numbers $b \geq 2$, $m$, and digit $d$ in the base $b$ expansion of $m$, we have $d < b$.

Nat.ofDigits_lt_base_pow_length' theorem

{b : ℕ} {l : List ℕ} (hl : ∀ x ∈ l, x < b + 2) : ofDigits (b + 2) l < (b + 2) ^ l.length

Full source

/-- an n-digit number in base b + 2 is less than (b + 2)^n -/
theorem ofDigits_lt_base_pow_length' {b : ℕ} {l : List ℕ} (hl : ∀ x ∈ l, x < b + 2) :
    ofDigits (b + 2) l < (b + 2) ^ l.length := by
  induction' l with hd tl IH
  · simp [ofDigits]
  · rw [ofDigits, List.length_cons, pow_succ]
    have : (ofDigits (b + 2) tl + 1) * (b + 2) ≤ (b + 2) ^ tl.length * (b + 2) :=
      mul_le_mul (IH fun x hx => hl _ (List.mem_cons_of_mem _ hx)) (by rfl) (by simp only [zero_le])
        (Nat.zero_le _)
    suffices ↑hd < b + 2 by linarith
    exact hl hd List.mem_cons_self

Upper Bound on Number Represented by Digits in Base $b+2$: $\text{ofDigits}_{b+2}(l) < (b+2)^{|l|}$

Informal description

For any natural number $b$ and list of natural numbers $l$, if every element $x$ in $l$ satisfies $x < b + 2$, then the number represented by $l$ in base $b + 2$ is less than $(b + 2)^{\text{length}(l)}$.

Nat.ofDigits_lt_base_pow_length theorem

{b : ℕ} {l : List ℕ} (hb : 1 < b) (hl : ∀ x ∈ l, x < b) : ofDigits b l < b ^ l.length

Full source

/-- an n-digit number in base b is less than b^n if b > 1 -/
theorem ofDigits_lt_base_pow_length {b : ℕ} {l : List ℕ} (hb : 1 < b) (hl : ∀ x ∈ l, x < b) :
    ofDigits b l < b ^ l.length := by
  rcases b with (_ | _ | b) <;> try simp_all
  exact ofDigits_lt_base_pow_length' hl

Upper Bound for Base-$b$ Digit Representation: $\text{ofDigits}_b(l) < b^{|l|}$

Informal description

For any natural number $b > 1$ and list of natural numbers $l$, if every digit $x \in l$ satisfies $x < b$, then the number represented by $l$ in base $b$ is strictly less than $b^{\text{length}(l)}$.

Nat.lt_base_pow_length_digits' theorem

{b m : ℕ} : m < (b + 2) ^ (digits (b + 2) m).length

Full source

/-- Any number m is less than (b+2)^(number of digits in the base b + 2 representation of m) -/
theorem lt_base_pow_length_digits' {b m : ℕ} : m < (b + 2) ^ (digits (b + 2) m).length := by
  convert @ofDigits_lt_base_pow_length' b (digits (b + 2) m) fun _ => digits_lt_base'
  rw [ofDigits_digits (b + 2) m]

Upper bound on natural numbers by base power of digit count: $m < (b+2)^{|\text{digits}_{b+2}(m)|}$

Informal description

For any natural numbers $b$ and $m$, the number $m$ is strictly less than $(b + 2)^{d}$, where $d$ is the number of digits in the base $b + 2$ representation of $m$.

Nat.lt_base_pow_length_digits theorem

{b m : ℕ} (hb : 1 < b) : m < b ^ (digits b m).length

Full source

/-- Any number m is less than b^(number of digits in the base b representation of m) -/
theorem lt_base_pow_length_digits {b m : ℕ} (hb : 1 < b) : m < b ^ (digits b m).length := by
  rcases b with (_ | _ | b) <;> try simp_all
  exact lt_base_pow_length_digits'

Upper bound on natural numbers by base power of digit count: $m < b^{|\text{digits}_b(m)|}$

Informal description

For any natural numbers $b > 1$ and $m$, the number $m$ is strictly less than $b^d$, where $d$ is the number of digits in the base $b$ representation of $m$.

Nat.digits_base_pow_mul theorem

{b k m : ℕ} (hb : 1 < b) (hm : 0 < m) : digits b (b ^ k * m) = List.replicate k 0 ++ digits b m

Full source

theorem digits_base_pow_mul {b k m : ℕ} (hb : 1 < b) (hm : 0 < m) :
    digits b (b ^ k * m) = List.replicate k 0 ++ digits b m := by
  induction k generalizing m with
  | zero => simp
  | succ k ih =>
    have hmb : 0 < m * b := lt_mul_of_lt_of_one_lt' hm hb
    let h1 := digits_def' hb hmb
    have h2 : m = m * b / b :=
      Nat.eq_div_of_mul_eq_left (ne_zero_of_lt hb) rfl
    simp only [mul_mod_left, ← h2] at h1
    rw [List.replicate_succ', List.append_assoc, List.singleton_append, ← h1, ← ih hmb]
    ring_nf

Digits of $b^k \cdot m$ in base $b$ consist of $k$ zeros followed by digits of $m$

Informal description

For any base $b > 1$, exponent $k \in \mathbb{N}$, and positive natural number $m > 0$, the digits of $b^k \cdot m$ in base $b$ are equal to the list obtained by concatenating $k$ zeros with the digits of $m$ in base $b$. That is, \[ \text{digits}_b(b^k \cdot m) = \underbrace{0 \cdots 0}_{k \text{ times}} +\!\!\!\!+\,\text{digits}_b(m) \] where $+\!\!\!\!+$ denotes list concatenation.

Nat.ofDigits_digits_append_digits theorem

{b m n : ℕ} : ofDigits b (digits b n ++ digits b m) = n + b ^ (digits b n).length * m

Full source

theorem ofDigits_digits_append_digits {b m n : ℕ} :
    ofDigits b (digits b n ++ digits b m) = n + b ^ (digits b n).length * m := by
  rw [ofDigits_append, ofDigits_digits, ofDigits_digits]

Reconstruction of Concatenated Digits in Base $b$: $\text{ofDigits}_b(\text{digits}_b(n) \text{++} \text{digits}_b(m)) = n + b^{k} m$

Informal description

For any natural numbers $b$, $m$, and $n$, interpreting the concatenation of the digits of $n$ in base $b$ followed by the digits of $m$ in base $b$ yields the value $n + b^{k} \cdot m$, where $k$ is the number of digits of $n$ in base $b$. That is, \[ \text{ofDigits}_b(\text{digits}_b(n) +\!\!\!\!+\, \text{digits}_b(m)) = n + b^{|\text{digits}_b(n)|} \cdot m \] where $+\!\!\!\!+$ denotes list concatenation and $|\cdot|$ denotes list length.

Nat.digits_append_digits theorem

{b m n : ℕ} (hb : 0 < b) : digits b n ++ digits b m = digits b (n + b ^ (digits b n).length * m)

Full source

theorem digits_append_digits {b m n : ℕ} (hb : 0 < b) :
    digits b n ++ digits b m = digits b (n + b ^ (digits b n).length * m) := by
  rcases eq_or_lt_of_le (Nat.succ_le_of_lt hb) with (rfl | hb)
  · simp
  rw [← ofDigits_digits_append_digits]
  refine (digits_ofDigits b hb _ (fun l hl => ?_) (fun h_append => ?_)).symm
  · rcases (List.mem_append.mp hl) with (h | h) <;> exact digits_lt_base hb h
  · by_cases h : digits b m = []
    · simp only [h, List.append_nil] at h_append ⊢
      exact getLast_digit_ne_zero b <| digits_ne_nil_iff_ne_zero.mp h_append
    · exact (List.getLast_append_of_right_ne_nil _ _ h) ▸
          (getLast_digit_ne_zero _ <| digits_ne_nil_iff_ne_zero.mp h)

Concatenation of Digits in Base $b$: $\mathrm{digits}_b(n) +\!\!\!\!+\, \mathrm{digits}_b(m) = \mathrm{digits}_b(n + b^{k}m)$ where $k = |\mathrm{digits}_b(n)|$

Informal description

For any natural numbers $b > 0$, $m$, and $n$, the concatenation of the digits of $n$ in base $b$ followed by the digits of $m$ in base $b$ equals the digits of $n + b^k \cdot m$ in base $b$, where $k$ is the number of digits of $n$ in base $b$. That is, \[ \mathrm{digits}_b(n) +\!\!\!\!+\, \mathrm{digits}_b(m) = \mathrm{digits}_b(n + b^{|\mathrm{digits}_b(n)|} \cdot m) \] where $+\!\!\!\!+$ denotes list concatenation and $|\cdot|$ denotes list length.

Nat.digits_append_zeroes_append_digits theorem

 {b k m n : ℕ} (hb : 1 < b) (hm : 0 < m) :
  digits b n ++ List.replicate k 0 ++ digits b m = digits b (n + b ^ ((digits b n).length + k) * m)

Full source

theorem digits_append_zeroes_append_digits {b k m n : ℕ} (hb : 1 < b) (hm : 0 < m) :
    digits b n ++ List.replicate k 0 ++ digits b m =
    digits b (n + b ^ ((digits b n).length + k) * m) := by
  rw [List.append_assoc, ← digits_base_pow_mul hb hm]
  simp only [digits_append_digits (zero_lt_of_lt hb), digits_inj_iff, add_right_inj]
  ring

Concatenation of Digits with Zeros in Base $b$: $\mathrm{digits}_b(n) +\!\!\!\!+\, 0^k +\!\!\!\!+\, \mathrm{digits}_b(m) = \mathrm{digits}_b(n + b^{k_1 + k} m)$ where $k_1 = |\mathrm{digits}_b(n)|$

Informal description

For any natural numbers $b > 1$, $k$, $m > 0$, and $n$, the concatenation of the digits of $n$ in base $b$, followed by $k$ zeros, followed by the digits of $m$ in base $b$, equals the digits of $n + b^{|\mathrm{digits}_b(n)| + k} \cdot m$ in base $b$. Here $|\mathrm{digits}_b(n)|$ denotes the length of the digits list of $n$ in base $b$.

Nat.digits_len_le_digits_len_succ theorem

(b n : ℕ) : (digits b n).length ≤ (digits b (n + 1)).length

Full source

theorem digits_len_le_digits_len_succ (b n : ℕ) :
    (digits b n).length ≤ (digits b (n + 1)).length := by
  rcases Decidable.eq_or_ne n 0 with (rfl | hn)
  · simp
  rcases le_or_lt b 1 with hb | hb
  · interval_cases b <;> simp +arith [digits_zero_succ', hn]
  simpa [digits_len, hb, hn] using log_mono_right (le_succ _)

Monotonicity of Digit Length: $\mathrm{length}(\mathrm{digits}_b(n)) \leq \mathrm{length}(\mathrm{digits}_b(n+1))$

Informal description

For any natural numbers $b$ and $n$, the length of the digits of $n$ in base $b$ is less than or equal to the length of the digits of $n+1$ in base $b$. In other words, the digit length function is non-decreasing with respect to incrementing the number.

Nat.le_digits_len_le theorem

(b n m : ℕ) (h : n ≤ m) : (digits b n).length ≤ (digits b m).length

Full source

theorem le_digits_len_le (b n m : ℕ) (h : n ≤ m) : (digits b n).length ≤ (digits b m).length :=
  monotone_nat_of_le_succ (digits_len_le_digits_len_succ b) h

Monotonicity of Digit Length: $\mathrm{length}(\mathrm{digits}_b(n)) \leq \mathrm{length}(\mathrm{digits}_b(m))$ for $n \leq m$

Informal description

For any natural numbers $b$, $n$, and $m$ such that $n \leq m$, the length of the digits of $n$ in base $b$ is less than or equal to the length of the digits of $m$ in base $b$. In other words, the digit length function is monotonic with respect to the natural number ordering.

Nat.ofDigits_monotone theorem

{p q : ℕ} (L : List ℕ) (h : p ≤ q) : ofDigits p L ≤ ofDigits q L

Full source

@[mono]
theorem ofDigits_monotone {p q : ℕ} (L : List ℕ) (h : p ≤ q) : ofDigits p L ≤ ofDigits q L := by
  induction L with
  | nil => rfl
  | cons _ _ hi =>
    simp only [ofDigits, cast_id, add_le_add_iff_left]
    exact Nat.mul_le_mul h hi

Monotonicity of Digit Interpretation with Respect to Base

Informal description

For any list of natural numbers $L$ and any natural numbers $p$ and $q$ such that $p \leq q$, the value of interpreting $L$ as digits in base $p$ is less than or equal to the value of interpreting $L$ as digits in base $q$. In other words, the function $\text{ofDigits}_p(L)$ is monotonic with respect to the base $p$.

Nat.sum_le_ofDigits theorem

{p : ℕ} (L : List ℕ) (h : 1 ≤ p) : L.sum ≤ ofDigits p L

Full source

theorem sum_le_ofDigits {p : ℕ} (L : List ℕ) (h : 1 ≤ p) : L.sum ≤ ofDigits p L :=
  (ofDigits_one L).symm ▸ ofDigits_monotone L h

Sum of Digits is Bounded by Base-$p$ Interpretation for $p \geq 1$

Informal description

For any list of natural numbers $L$ and any natural number $p \geq 1$, the sum of the elements of $L$ is less than or equal to the value obtained by interpreting $L$ as digits in base $p$, i.e., $\sum L \leq \text{ofDigits}_p(L)$.

Nat.digit_sum_le theorem

(p n : ℕ) : List.sum (digits p n) ≤ n

Full source

theorem digit_sum_le (p n : ℕ) : List.sum (digits p n) ≤ n := by
  induction' n with n
  · exact digits_zero _ ▸ Nat.le_refl (List.sum [])
  · induction' p with p
    · rw [digits_zero_succ, List.sum_cons, List.sum_nil, add_zero]
    · nth_rw 2 [← ofDigits_digits p.succ (n + 1)]
      rw [← ofDigits_one <| digits p.succ n.succ]
      exact ofDigits_monotone (digits p.succ n.succ) <| Nat.succ_pos p

Sum of Digits Bound in Base $p$

Informal description

For any natural numbers $p$ and $n$, the sum of the digits of $n$ in base $p$ is less than or equal to $n$, i.e., $$\sum (\mathrm{digits}_p(n)) \leq n.$$

Nat.pow_length_le_mul_ofDigits theorem

 {b : ℕ} {l : List ℕ} (hl : l ≠ []) (hl2 : l.getLast hl ≠ 0) : (b + 2) ^ l.length ≤ (b + 2) * ofDigits (b + 2) l

Full source

theorem pow_length_le_mul_ofDigits {b : ℕ} {l : List ℕ} (hl : l ≠ []) (hl2 : l.getLast hl ≠ 0) :
    (b + 2) ^ l.length ≤ (b + 2) * ofDigits (b + 2) l := by
  rw [← List.dropLast_append_getLast hl]
  simp only [List.length_append, List.length, zero_add, List.length_dropLast, ofDigits_append,
    List.length_dropLast, ofDigits_singleton, add_comm (l.length - 1), pow_add, pow_one]
  apply Nat.mul_le_mul_left
  refine le_trans ?_ (Nat.le_add_left _ _)
  have : 0 < l.getLast hl := by rwa [pos_iff_ne_zero]
  convert Nat.mul_le_mul_left ((b + 2) ^ (l.length - 1)) this using 1
  rw [Nat.mul_one]

Exponential Length Bound for Non-Zero Digits in Base $b+2$

Informal description

For any natural number base $b$ and non-empty list of natural numbers $l$ whose last element is non-zero, the inequality $(b + 2)^{|l|} \leq (b + 2) \cdot \text{ofDigits}_{b+2}(l)$ holds, where $|l|$ denotes the length of $l$ and $\text{ofDigits}_{b+2}(l)$ is the number obtained by interpreting $l$ as digits in base $b+2$.

Nat.base_pow_length_digits_le' theorem

(b m : ℕ) (hm : m ≠ 0) : (b + 2) ^ (digits (b + 2) m).length ≤ (b + 2) * m

Full source

/-- Any non-zero natural number `m` is greater than
(b+2)^((number of digits in the base (b+2) representation of m) - 1)
-/
theorem base_pow_length_digits_le' (b m : ℕ) (hm : m ≠ 0) :
    (b + 2) ^ (digits (b + 2) m).length ≤ (b + 2) * m := by
  have : digitsdigits (b + 2) m ≠ [] := digits_ne_nil_iff_ne_zero.mpr hm
  convert @pow_length_le_mul_ofDigits b (digits (b+2) m)
    this (getLast_digit_ne_zero _ hm)
  rw [ofDigits_digits]

Exponential Lower Bound on Number Size in Base $(b+2)$

Informal description

For any natural numbers $b$ and $m$ with $m \neq 0$, the inequality $(b + 2)^{|\mathrm{digits}_{b+2}(m)|} \leq (b + 2) \cdot m$ holds, where $|\mathrm{digits}_{b+2}(m)|$ denotes the number of digits in the base $(b+2)$ representation of $m$.

Nat.base_pow_length_digits_le theorem

(b m : ℕ) (hb : 1 < b) : m ≠ 0 → b ^ (digits b m).length ≤ b * m

Full source

/-- Any non-zero natural number `m` is greater than
b^((number of digits in the base b representation of m) - 1)
-/
theorem base_pow_length_digits_le (b m : ℕ) (hb : 1 < b) :
    m ≠ 0 → b ^ (digits b m).length ≤ b * m := by
  rcases b with (_ | _ | b) <;> try simp_all
  exact base_pow_length_digits_le' b m

Exponential Lower Bound on Number Size in Base $b$

Informal description

For any natural numbers $b > 1$ and $m \neq 0$, the inequality $b^{|\mathrm{digits}_b(m)|} \leq b \cdot m$ holds, where $|\mathrm{digits}_b(m)|$ denotes the number of digits in the base $b$ representation of $m$.

Nat.ofDigits_div_eq_ofDigits_tail theorem

 {p : ℕ} (hpos : 0 < p) (digits : List ℕ) (w₁ : ∀ l ∈ digits, l < p) : ofDigits p digits / p = ofDigits p digits.tail

Full source

/-- Interpreting as a base `p` number and dividing by `p` is the same as interpreting the tail.
-/
lemma ofDigits_div_eq_ofDigits_tail {p : ℕ} (hpos : 0 < p) (digits : List ℕ)
    (w₁ : ∀ l ∈ digits, l < p) : ofDigits p digits / p = ofDigits p digits.tail := by
  induction' digits with hd tl
  · simp [ofDigits]
  · refine Eq.trans (add_mul_div_left hd _ hpos) ?_
    rw [Nat.div_eq_of_lt <| w₁ _ List.mem_cons_self, zero_add]
    rfl

Division by Base Equals Interpretation of Tail in Base $p$

Informal description

Let $p$ be a positive natural number and let $\text{digits}$ be a list of natural numbers where each digit is less than $p$. Then the interpretation of $\text{digits}$ as a base $p$ number divided by $p$ is equal to the interpretation of the tail of $\text{digits}$ as a base $p$ number. In other words: \[ \text{ofDigits}_p(\text{digits}) / p = \text{ofDigits}_p(\text{digits.tail}) \]

Nat.ofDigits_div_pow_eq_ofDigits_drop theorem

 {p : ℕ} (i : ℕ) (hpos : 0 < p) (digits : List ℕ) (w₁ : ∀ l ∈ digits, l < p) :
  ofDigits p digits / p ^ i = ofDigits p (digits.drop i)

Full source

/-- Interpreting as a base `p` number and dividing by `p^i` is the same as dropping `i`.
-/
lemma ofDigits_div_pow_eq_ofDigits_drop
    {p : ℕ} (i : ℕ) (hpos : 0 < p) (digits : List ℕ) (w₁ : ∀ l ∈ digits, l < p) :
    ofDigits p digits / p ^ i = ofDigits p (digits.drop i) := by
  induction' i with i hi
  · simp
  · rw [Nat.pow_succ, ← Nat.div_div_eq_div_mul, hi, ofDigits_div_eq_ofDigits_tail hpos
      (List.drop i digits) fun x hx ↦ w₁ x <| List.mem_of_mem_drop hx, ← List.drop_one,
      List.drop_drop, add_comm]

Division by Power of Base Equals Interpretation of Dropped Digits in Base $p$

Informal description

Let $p$ be a positive natural number and let $\text{digits}$ be a list of natural numbers where each digit is less than $p$. Then for any natural number $i$, the interpretation of $\text{digits}$ as a base $p$ number divided by $p^i$ is equal to the interpretation of the list obtained by dropping the first $i$ digits of $\text{digits}$ as a base $p$ number. In other words: \[ \text{ofDigits}_p(\text{digits}) / p^i = \text{ofDigits}_p(\text{digits.drop } i) \]

Nat.self_div_pow_eq_ofDigits_drop theorem

{p : ℕ} (i n : ℕ) (h : 2 ≤ p) : n / p ^ i = ofDigits p ((p.digits n).drop i)

Full source

/-- Dividing `n` by `p^i` is like truncating the first `i` digits of `n` in base `p`.
-/
lemma self_div_pow_eq_ofDigits_drop {p : ℕ} (i n : ℕ) (h : 2 ≤ p) :
    n / p ^ i = ofDigits p ((p.digits n).drop i) := by
  convert ofDigits_div_pow_eq_ofDigits_drop i (zero_lt_of_lt h) (p.digits n)
    (fun l hl ↦ digits_lt_base h hl)
  exact (ofDigits_digits p n).symm

Division by Power of Base Equals Interpretation of Dropped Digits

Informal description

For any natural numbers $p \geq 2$, $i$, and $n$, the integer division of $n$ by $p^i$ equals the number obtained by interpreting the digits of $n$ in base $p$ after dropping the first $i$ digits. In other words: \[ n / p^i = \text{ofDigits}_p(\text{digits}_p(n).\text{drop } i) \]

Nat.sub_one_mul_sum_div_pow_eq_sub_sum_digits theorem

 {p : ℕ} (L : List ℕ) {h_nonempty} (h_ne_zero : L.getLast h_nonempty ≠ 0) (h_lt : ∀ l ∈ L, l < p) :
  (p - 1) * ∑ i ∈ range L.length, (ofDigits p L) / p ^ i.succ = (ofDigits p L) - L.sum

Full source

theorem sub_one_mul_sum_div_pow_eq_sub_sum_digits {p : ℕ}
    (L : List ℕ) {h_nonempty} (h_ne_zero : L.getLast h_nonempty ≠ 0) (h_lt : ∀ l ∈ L, l < p) :
    (p - 1) * ∑ i ∈ range L.length, (ofDigits p L) / p ^ i.succ = (ofDigits p L) - L.sum := by
  obtain h | rfl | h : 1 < p ∨ 1 = p ∨ p < 1 := trichotomous 1 p
  · induction' L with hd tl ih
    · simp [ofDigits]
    · simp only [List.length_cons, List.sum_cons, self_div_pow_eq_ofDigits_drop _ _ h,
          digits_ofDigits p h (hd :: tl) h_lt (fun _ => h_ne_zero)]
      simp only [ofDigits]
      rw [sum_range_succ, Nat.cast_id]
      simp only [List.drop, List.drop_length]
      obtain rfl | h' := em <| tl = []
      · simp [ofDigits]
      · have w₁' := fun l hl ↦ h_lt l <| List.mem_cons_of_mem hd hl
        have w₂' := fun (h : tl ≠ []) ↦ (List.getLast_cons h) ▸ h_ne_zero
        have ih := ih (w₂' h') w₁'
        simp only [self_div_pow_eq_ofDigits_drop _ _ h, digits_ofDigits p h tl w₁' w₂',
          ← Nat.one_add] at ih
        have := sum_singleton (fun x ↦ ofDigits p <| tl.drop x) tl.length
        rw [← Ico_succ_singleton, List.drop_length, ofDigits] at this
        have h₁ : 1 ≤ tl.length := List.length_pos_iff.mpr h'
        rw [← sum_range_add_sum_Ico _ <| h₁, ← add_zero (∑ x ∈ Ico _ _, ofDigits p (tl.drop x)),
            ← this, sum_Ico_consecutive _  h₁ <| (le_add_right tl.length 1),
            ← sum_Ico_add _ 0 tl.length 1,
            Ico_zero_eq_range, mul_add, mul_add, ih, range_one, sum_singleton, List.drop, ofDigits,
            mul_zero, add_zero, ← Nat.add_sub_assoc <| sum_le_ofDigits _ <| Nat.le_of_lt h]
        nth_rw 2 [← one_mul <| ofDigits p tl]
        rw [← add_mul, Nat.sub_add_cancel (one_le_of_lt h), Nat.add_sub_add_left]
  · simp [ofDigits_one]
  · simp [lt_one_iff.mp h]
    cases L
    · rfl
    · simp [ofDigits]

Digit Sum Identity: $(p-1)\sum_i \frac{N}{p^{i+1}} = N - \text{sum of digits}$ for Base-$p$ Number $N$

Informal description

For any natural number base $p$ and any non-empty list of digits $L$ in base $p$ (where each digit $l \in L$ satisfies $l < p$ and the last digit is non-zero), the following identity holds: $$(p - 1) \cdot \sum_{i=0}^{\mathrm{length}(L)-1} \frac{\mathrm{ofDigits}_p(L)}{p^{i+1}} = \mathrm{ofDigits}_p(L) - \sum L.$$ Here $\mathrm{ofDigits}_p(L)$ denotes the number obtained by interpreting $L$ as digits in base $p$ (least significant digit first), and $\sum L$ is the sum of the digits in $L$.

Nat.sub_one_mul_sum_log_div_pow_eq_sub_sum_digits theorem

{p : ℕ} (n : ℕ) : (p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum

Full source

theorem sub_one_mul_sum_log_div_pow_eq_sub_sum_digits {p : ℕ} (n : ℕ) :
    (p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum := by
  obtain h | rfl | h : 1 < p ∨ 1 = p ∨ p < 1 := trichotomous 1 p
  · rcases eq_or_ne n 0 with rfl | hn
    · simp
    · convert sub_one_mul_sum_div_pow_eq_sub_sum_digits (p.digits n) (getLast_digit_ne_zero p hn) <|
          (fun l a ↦ digits_lt_base h a)
      · refine (digits_len p n h hn).symm
      all_goals exact (ofDigits_digits p n).symm
  · simp
  · simp [lt_one_iff.mp h]
    cases n
    all_goals simp

Digit Sum Identity: $(p-1)\sum_{i=0}^{\log_p n} \frac{n}{p^{i+1}} = n - \text{sum of digits}$

Informal description

For any natural numbers $p$ and $n$, the following identity holds: $$(p - 1) \cdot \sum_{i=0}^{\log_p n} \frac{n}{p^{i+1}} = n - \sum (\mathrm{digits}_p(n)),$$ where $\mathrm{digits}_p(n)$ denotes the list of digits of $n$ in base $p$ (least significant digit first) and $\sum (\mathrm{digits}_p(n))$ is the sum of these digits.

Nat.digits_two_eq_bits theorem

(n : ℕ) : digits 2 n = n.bits.map fun b => cond b 1 0

Full source

theorem digits_two_eq_bits (n : ℕ) : digits 2 n = n.bits.map fun b => cond b 1 0 := by
  induction' n using Nat.binaryRecFromOne with b n h ih
  · simp
  · simp
  rw [bits_append_bit _ _ fun hn => absurd hn h]
  cases b
  · rw [digits_def' one_lt_two]
    · simpa [Nat.bit]
    · simpa [Nat.bit, pos_iff_ne_zero]
  · simpa [Nat.bit, add_comm, digits_add 2 one_lt_two 1 n, Nat.add_mul_div_left]

Base-2 Digits as Mapped Binary Bits: $\mathrm{digits}_2(n) = \mathrm{bits}(n).\mathrm{map}(b \mapsto \mathrm{if}\, b\, \mathrm{then}\, 1\, \mathrm{else}\, 0)$

Informal description

For any natural number $n$, the digits of $n$ in base $2$ are equal to the list obtained by mapping each boolean value in the binary representation of $n$ (least significant bit first) to $1$ if the bit is true and $0$ otherwise. That is, \[ \mathrm{digits}_2(n) = \mathrm{map} \, (\lambda b. \, \mathrm{if} \, b \, \mathrm{then} \, 1 \, \mathrm{else} \, 0) \, (\mathrm{bits}(n)). \]

Nat.dvd_ofDigits_sub_ofDigits theorem

{α : Type*} [CommRing α] {a b k : α} (h : k ∣ a - b) (L : List ℕ) : k ∣ ofDigits a L - ofDigits b L

Full source

theorem dvd_ofDigits_sub_ofDigits {α : Type*} [CommRing α] {a b k : α} (h : k ∣ a - b)
    (L : List ℕ) : k ∣ ofDigits a L - ofDigits b L := by
  induction' L with d L ih
  · change k ∣ 0 - 0
    simp
  · simp only [ofDigits, add_sub_add_left_eq_sub]
    exact dvd_mul_sub_mul h ih

Divisibility of Digit Interpretation Differences in Commutative Rings

Informal description

Let $\alpha$ be a commutative ring, and let $a, b, k \in \alpha$ such that $k$ divides $a - b$. Then for any list of natural numbers $L$, the difference between interpreting $L$ as digits in base $a$ and interpreting $L$ as digits in base $b$ is divisible by $k$. In other words, $k$ divides $\text{ofDigits}(a, L) - \text{ofDigits}(b, L)$.

Nat.ofDigits_modEq' theorem

(b b' : ℕ) (k : ℕ) (h : b ≡ b' [MOD k]) (L : List ℕ) : ofDigits b L ≡ ofDigits b' L [MOD k]

Full source

theorem ofDigits_modEq' (b b' : ℕ) (k : ℕ) (h : b ≡ b' [MOD k]) (L : List ℕ) :
    ofDigitsofDigits b L ≡ ofDigits b' L [MOD k] := by
  induction' L with d L ih
  · rfl
  · dsimp [ofDigits]
    dsimp [Nat.ModEq] at *
    conv_lhs => rw [Nat.add_mod, Nat.mul_mod, h, ih]
    conv_rhs => rw [Nat.add_mod, Nat.mul_mod]

Congruence of Digit Interpretations Under Base Change Modulo $k$

Informal description

Let $b$, $b'$, and $k$ be natural numbers such that $b \equiv b' \pmod{k}$. Then for any list of natural numbers $L$, the number represented by interpreting $L$ as digits in base $b$ is congruent modulo $k$ to the number represented by interpreting $L$ as digits in base $b'$. In other words, $\text{ofDigits}(b, L) \equiv \text{ofDigits}(b', L) \pmod{k}$.

Nat.ofDigits_modEq theorem

(b k : ℕ) (L : List ℕ) : ofDigits b L ≡ ofDigits (b % k) L [MOD k]

Full source

theorem ofDigits_modEq (b k : ℕ) (L : List ℕ) : ofDigitsofDigits b L ≡ ofDigits (b % k) L [MOD k] :=
  ofDigits_modEq' b (b % k) k (b.mod_modEq k).symm L

Congruence of Digit Interpretations Under Base Reduction Modulo $k$

Informal description

For any natural numbers $b$ and $k$, and any list of natural numbers $L$, the number obtained by interpreting $L$ as digits in base $b$ is congruent modulo $k$ to the number obtained by interpreting $L$ as digits in base $(b \mod k)$. In other words: \[ \text{ofDigits}(b, L) \equiv \text{ofDigits}(b \mod k, L) \pmod{k} \]

Nat.ofDigits_mod theorem

(b k : ℕ) (L : List ℕ) : ofDigits b L % k = ofDigits (b % k) L % k

Full source

theorem ofDigits_mod (b k : ℕ) (L : List ℕ) : ofDigits b L % k = ofDigits (b % k) L % k :=
  ofDigits_modEq b k L

Modular Equivalence of Digit Interpretations Under Base Reduction

Informal description

For any natural numbers $b$ and $k$, and any list of natural numbers $L$, the remainder when interpreting $L$ as digits in base $b$ and dividing by $k$ is equal to the remainder when interpreting $L$ as digits in base $(b \mod k)$ and dividing by $k$. In other words: \[ \text{ofDigits}(b, L) \mod k = \text{ofDigits}(b \mod k, L) \mod k \]

Nat.ofDigits_mod_eq_head! theorem

(b : ℕ) (l : List ℕ) : ofDigits b l % b = l.head! % b

Full source

theorem ofDigits_mod_eq_head! (b : ℕ) (l : List ℕ) : ofDigits b l % b = l.head! % b := by
  induction l <;> simp [Nat.ofDigits, Int.ModEq]

Modular Property of Little-Endian Digits: $\text{ofDigits}(b, l) \mod b = l_0 \mod b$

Informal description

For any natural number base $b$ and list of digits $l$ (represented as natural numbers), the value of $\text{ofDigits}(b, l)$ modulo $b$ is equal to the first digit of $l$ modulo $b$. In other words, \[ \text{ofDigits}(b, l) \mod b = l_0 \mod b, \] where $l_0$ is the first element of the list $l$ (or $0$ if $l$ is empty).

Nat.head!_digits theorem

{b n : ℕ} (h : b ≠ 1) : (Nat.digits b n).head! = n % b

Full source

theorem head!_digits {b n : ℕ} (h : b ≠ 1) : (Nat.digits b n).head! = n % b := by
  by_cases hb : 1 < b
  · rcases n with _ | n
    · simp
    · nth_rw 2 [← Nat.ofDigits_digits b (n + 1)]
      rw [Nat.ofDigits_mod_eq_head! _ _]
      exact (Nat.mod_eq_of_lt (Nat.digits_lt_base hb <| List.head!_mem_self <|
          Nat.digits_ne_nil_iff_ne_zero.mpr <| Nat.succ_ne_zero n)).symm
  · rcases n with _ | _ <;> simp_all [show b = 0 by omega]

Least Significant Digit Equals Modulo Base: $\text{head}(\text{digits}_b(n)) = n \mod b$ for $b \neq 1$

Informal description

For any natural numbers $b \neq 1$ and $n$, the first digit (least significant digit) in the base $b$ representation of $n$ is equal to $n$ modulo $b$. That is, \[ \text{head}(\text{digits}_b(n)) = n \mod b, \] where $\text{head}(L)$ denotes the first element of list $L$ (or $0$ if $L$ is empty).

Nat.ofDigits_zmodeq' theorem

(b b' : ℤ) (k : ℕ) (h : b ≡ b' [ZMOD k]) (L : List ℕ) : ofDigits b L ≡ ofDigits b' L [ZMOD k]

Full source

theorem ofDigits_zmodeq' (b b' : ℤ) (k : ℕ) (h : b ≡ b' [ZMOD k]) (L : List ℕ) :
    ofDigitsofDigits b L ≡ ofDigits b' L [ZMOD k] := by
  induction' L with d L ih
  · rfl
  · dsimp [ofDigits]
    dsimp [Int.ModEq] at *
    conv_lhs => rw [Int.add_emod, Int.mul_emod, h, ih]
    conv_rhs => rw [Int.add_emod, Int.mul_emod]

Congruence of Digit Interpretations under Base Change Modulo $k$

Informal description

For any integers $b$, $b'$ and natural number $k$, if $b \equiv b' \pmod{k}$, then for any list of natural numbers $L$, the interpretation of $L$ as digits in base $b$ is congruent modulo $k$ to the interpretation of $L$ as digits in base $b'$. That is, \[ \text{ofDigits}(b, L) \equiv \text{ofDigits}(b', L) \pmod{k}. \]

Nat.ofDigits_zmodeq theorem

(b : ℤ) (k : ℕ) (L : List ℕ) : ofDigits b L ≡ ofDigits (b % k) L [ZMOD k]

Full source

theorem ofDigits_zmodeq (b : ℤ) (k : ℕ) (L : List ℕ) : ofDigitsofDigits b L ≡ ofDigits (b % k) L [ZMOD k] :=
  ofDigits_zmodeq' b (b % k) k (b.mod_modEq ↑k).symm L

Congruence of Digit Interpretations under Base Reduction Modulo $k$

Informal description

For any integer $b$, natural number $k$, and list of natural numbers $L$, the interpretation of $L$ as digits in base $b$ is congruent modulo $k$ to the interpretation of $L$ as digits in base $(b \% k)$. That is, \[ \text{ofDigits}(b, L) \equiv \text{ofDigits}(b \% k, L) \pmod{k}. \]

Nat.ofDigits_zmod theorem

(b : ℤ) (k : ℕ) (L : List ℕ) : ofDigits b L % k = ofDigits (b % k) L % k

Full source

theorem ofDigits_zmod (b : ℤ) (k : ℕ) (L : List ℕ) : ofDigits b L % k = ofDigits (b % k) L % k :=
  ofDigits_zmodeq b k L

Modular Equivalence of Digit Interpretations under Base Reduction

Informal description

For any integer base $b$, natural number $k$, and list of natural numbers $L$, the remainder when interpreting $L$ as digits in base $b$ and taking modulo $k$ is equal to the remainder when interpreting $L$ as digits in base $(b \% k)$ and taking modulo $k$. That is, \[ \text{ofDigits}(b, L) \mod k = \text{ofDigits}(b \% k, L) \mod k. \]

Nat.modEq_digits_sum theorem

(b b' : ℕ) (h : b' % b = 1) (n : ℕ) : n ≡ (digits b' n).sum [MOD b]

Full source

theorem modEq_digits_sum (b b' : ℕ) (h : b' % b = 1) (n : ℕ) : n ≡ (digits b' n).sum [MOD b] := by
  rw [← ofDigits_one]
  conv =>
    congr
    · skip
    · rw [← ofDigits_digits b' n]
  convert ofDigits_modEq b' b (digits b' n)
  exact h.symm

Congruence of Number Modulo $b$ to Sum of Its Digits in Base $b'$ When $b' \equiv 1 \pmod{b}$

Informal description

For any natural numbers $b$ and $b'$ such that $b' \equiv 1 \pmod{b}$ (i.e., $b' \mod b = 1$), and for any natural number $n$, we have the congruence: $$n \equiv \sum (\text{digits}_{b'}(n)) \pmod{b},$$ where $\text{digits}_{b'}(n)$ denotes the digits of $n$ in base $b'$ and $\sum$ denotes the sum of these digits.

Nat.modEq_three_digits_sum theorem

(n : ℕ) : n ≡ (digits 10 n).sum [MOD 3]

Full source

theorem modEq_three_digits_sum (n : ℕ) : n ≡ (digits 10 n).sum [MOD 3] :=
  modEq_digits_sum 3 10 (by norm_num) n

Divisibility by 3 Test via Digit Sum in Base 10

Informal description

For any natural number $n$, the number $n$ is congruent modulo 3 to the sum of its digits in base 10, i.e., $$n \equiv \sum (\text{digits}_{10}(n)) \pmod{3}.$$

Nat.modEq_nine_digits_sum theorem

(n : ℕ) : n ≡ (digits 10 n).sum [MOD 9]

Full source

theorem modEq_nine_digits_sum (n : ℕ) : n ≡ (digits 10 n).sum [MOD 9] :=
  modEq_digits_sum 9 10 (by norm_num) n

Divisibility by 9 Test via Digit Sum in Base 10

Informal description

For any natural number $n$, the number $n$ is congruent modulo $9$ to the sum of its digits in base $10$. That is, $$n \equiv \sum (\text{digits}_{10}(n)) \pmod{9},$$ where $\text{digits}_{10}(n)$ denotes the digits of $n$ in base $10$.

Nat.zmodeq_ofDigits_digits theorem

(b b' : ℕ) (c : ℤ) (h : b' ≡ c [ZMOD b]) (n : ℕ) : n ≡ ofDigits c (digits b' n) [ZMOD b]

Full source

theorem zmodeq_ofDigits_digits (b b' : ℕ) (c : ℤ) (h : b' ≡ c [ZMOD b]) (n : ℕ) :
    n ≡ ofDigits c (digits b' n) [ZMOD b] := by
  conv =>
    congr
    · skip
    · rw [← ofDigits_digits b' n]
  rw [coe_int_ofDigits]
  apply ofDigits_zmodeq' _ _ _ h

Congruence of Number to Its Digit Interpretation under Base Change Modulo $b$

Informal description

For any natural numbers $b$ and $b'$, integer $c$, and natural number $n$, if $b' \equiv c \pmod{b}$, then $n \equiv \text{ofDigits}_c(\text{digits}_{b'}(n)) \pmod{b}$.

Nat.ofDigits_neg_one theorem

: ∀ L : List ℕ, ofDigits (-1 : ℤ) L = (L.map fun n : ℕ => (n : ℤ)).alternatingSum

Full source

theorem ofDigits_neg_one :
    ∀ L : List ℕ, ofDigits (-1 : ℤ) L = (L.map fun n : ℕ => (n : ℤ)).alternatingSum
  | [] => rfl
  | [n] => by simp [ofDigits, List.alternatingSum]
  | a :: b :: t => by
    simp only [ofDigits, List.alternatingSum, List.map_cons, ofDigits_neg_one t]
    ring

Alternating Sum Representation of Digits in Base $-1$

Informal description

For any list $L$ of natural numbers, interpreting $L$ as digits in base $-1$ (using the `ofDigits` function) yields the alternating sum of the elements of $L$ when each element is viewed as an integer. That is, $\text{ofDigits}\,(-1)\, L = \text{alternatingSum}\,(\text{map}\,(\text{coe}\, : \mathbb{N} \to \mathbb{Z})\, L)$.

Nat.modEq_eleven_digits_sum theorem

(n : ℕ) : n ≡ ((digits 10 n).map fun n : ℕ => (n : ℤ)).alternatingSum [ZMOD 11]

Full source

theorem modEq_eleven_digits_sum (n : ℕ) :
    n ≡ ((digits 10 n).map fun n : ℕ => (n : ℤ)).alternatingSum [ZMOD 11] := by
  have t := zmodeq_ofDigits_digits 11 10 (-1 : ℤ) (by unfold Int.ModEq; rfl) n
  rwa [ofDigits_neg_one] at t

Divisibility by 11 Rule via Alternating Digit Sum in Base 10

Informal description

For any natural number $n$, the congruence relation $n \equiv \text{alternatingSum}(\text{map}\,(\text{coe}\, : \mathbb{N} \to \mathbb{Z})\, (\text{digits}_{10}(n))) \pmod{11}$ holds, where $\text{alternatingSum}$ denotes the alternating sum of the digits of $n$ in base 10 when interpreted as integers.

Nat.dvd_iff_dvd_digits_sum theorem

(b b' : ℕ) (h : b' % b = 1) (n : ℕ) : b ∣ n ↔ b ∣ (digits b' n).sum

Full source

theorem dvd_iff_dvd_digits_sum (b b' : ℕ) (h : b' % b = 1) (n : ℕ) :
    b ∣ nb ∣ n ↔ b ∣ (digits b' n).sum := by
  rw [← ofDigits_one]
  conv_lhs => rw [← ofDigits_digits b' n]
  rw [Nat.dvd_iff_mod_eq_zero, Nat.dvd_iff_mod_eq_zero, ofDigits_mod, h]

Divisibility Test via Digit Sum in Congruent Base

Informal description

For any natural numbers $b$, $b'$ with $b' \equiv 1 \mod b$, and any natural number $n$, the number $b$ divides $n$ if and only if $b$ divides the sum of the digits of $n$ in base $b'$. In other words: $$ b \mid n \leftrightarrow b \mid \left(\sum_{d \in \text{digits}_{b'}(n)} d\right) $$

Nat.three_dvd_iff theorem

(n : ℕ) : 3 ∣ n ↔ 3 ∣ (digits 10 n).sum

Full source

/-- **Divisibility by 3 Rule** -/
theorem three_dvd_iff (n : ℕ) : 3 ∣ n3 ∣ n ↔ 3 ∣ (digits 10 n).sum :=
  dvd_iff_dvd_digits_sum 3 10 (by norm_num) n

Divisibility by 3 Rule via Digit Sum

Informal description

For any natural number $n$, the number $3$ divides $n$ if and only if $3$ divides the sum of the digits of $n$ in base $10$. In other words: $$ 3 \mid n \leftrightarrow 3 \mid \left(\sum_{d \in \text{digits}_{10}(n)} d\right) $$

Nat.nine_dvd_iff theorem

(n : ℕ) : 9 ∣ n ↔ 9 ∣ (digits 10 n).sum

Full source

theorem nine_dvd_iff (n : ℕ) : 9 ∣ n9 ∣ n ↔ 9 ∣ (digits 10 n).sum :=
  dvd_iff_dvd_digits_sum 9 10 (by norm_num) n

Divisibility by 9 via Digit Sum in Base 10

Informal description

For any natural number $n$, the number $9$ divides $n$ if and only if $9$ divides the sum of the digits of $n$ in base $10$. In other words: $$ 9 \mid n \leftrightarrow 9 \mid \left(\sum_{d \in \text{digits}_{10}(n)} d\right) $$

Nat.dvd_iff_dvd_ofDigits theorem

 (b b' : ℕ) (c : ℤ) (h : (b : ℤ) ∣ (b' : ℤ) - c) (n : ℕ) : b ∣ n ↔ (b : ℤ) ∣ ofDigits c (digits b' n)

Full source

theorem dvd_iff_dvd_ofDigits (b b' : ℕ) (c : ℤ) (h : (b : ℤ) ∣ (b' : ℤ) - c) (n : ℕ) :
    b ∣ nb ∣ n ↔ (b : ℤ) ∣ ofDigits c (digits b' n) := by
  rw [← Int.natCast_dvd_natCast]
  exact
    dvd_iff_dvd_of_dvd_sub (zmodeq_ofDigits_digits b b' c (Int.modEq_iff_dvd.2 h).symm _).symm.dvd

Divisibility via Digit Interpretation in Modified Base

Informal description

For natural numbers $b$ and $b'$, an integer $c$, and a natural number $n$, if $b$ divides $b' - c$ (as integers), then $b$ divides $n$ if and only if $b$ divides the number obtained by interpreting the digits of $n$ in base $b'$ as a number in base $c$. More precisely, let $L = \text{digits}_{b'}(n)$ be the digits of $n$ in base $b'$, and let $\text{ofDigits}_c(L)$ be the number obtained by interpreting $L$ in base $c$. Then: $$ b \mid n \leftrightarrow b \mid \text{ofDigits}_c(L) $$

Nat.eleven_dvd_iff theorem

: 11 ∣ n ↔ (11 : ℤ) ∣ ((digits 10 n).map fun n : ℕ => (n : ℤ)).alternatingSum

Full source

theorem eleven_dvd_iff :
    11 ∣ n11 ∣ n ↔ (11 : ℤ) ∣ ((digits 10 n).map fun n : ℕ => (n : ℤ)).alternatingSum := by
  have t := dvd_iff_dvd_ofDigits 11 10 (-1 : ℤ) (by norm_num) n
  rw [ofDigits_neg_one] at t
  exact t

Divisibility by 11 via Alternating Digit Sum in Base 10

Informal description

For any natural number $n$, the number $11$ divides $n$ if and only if $11$ divides the alternating sum of the digits of $n$ in base $10$ (interpreted as integers). More precisely, if $L = \text{digits}_{10}(n)$ is the list of digits of $n$ in base $10$, then: $$ 11 \mid n \leftrightarrow 11 \mid \left(\sum_{i=0}^{k-1} (-1)^i \cdot L_i\right) $$ where $L_i$ denotes the $i$-th digit of $n$ (starting from the least significant digit).

Nat.eleven_dvd_of_palindrome theorem

(p : (digits 10 n).Palindrome) (h : Even (digits 10 n).length) : 11 ∣ n

Full source

theorem eleven_dvd_of_palindrome (p : (digits 10 n).Palindrome) (h : Even (digits 10 n).length) :
    11 ∣ n := by
  let dig := (digits 10 n).map fun n : ℕ => (n : ℤ)
  replace h : Even dig.length := by rwa [List.length_map]
  refine eleven_dvd_iff.2 ⟨0, (?_ : dig.alternatingSum = 0)⟩
  have := dig.alternatingSum_reverse
  rw [(p.map _).reverse_eq, _root_.pow_succ', h.neg_one_pow, mul_one, neg_one_zsmul] at this
  exact eq_zero_of_neg_eq this.symm

Divisibility by 11 for Even-Length Palindromic Numbers in Base 10

Informal description

For any natural number $n$, if the digits of $n$ in base $10$ form a palindrome and the number of digits is even, then $11$ divides $n$.

Nat.toDigitsCore_lens_eq_aux theorem

 (b f : Nat) :
  ∀ (n : Nat) (l1 l2 : List Char),
    l1.length = l2.length → (Nat.toDigitsCore b f n l1).length = (Nat.toDigitsCore b f n l2).length

Full source

lemma toDigitsCore_lens_eq_aux (b f : Nat) :
    ∀ (n : Nat) (l1 l2 : List Char), l1.length = l2.length →
    (Nat.toDigitsCore b f n l1).length = (Nat.toDigitsCore b f n l2).length := by
  induction f with (simp only [Nat.toDigitsCore, List.length]; intro n l1 l2 hlen)
  | zero => assumption
  | succ f ih =>
    if hx : n / b = 0 then
      simp only [hx, if_true, List.length, congrArg (fun l ↦ l + 1) hlen]
    else
      simp only [hx, if_false]
      specialize ih (n / b) (Nat.digitCharNat.digitChar (n % b) :: l1) (Nat.digitCharNat.digitChar (n % b) :: l2)
      simp only [List.length, congrArg (fun l ↦ l + 1) hlen] at ih
      exact ih trivial

Length Preservation in `Nat.toDigitsCore` for Equal-Length Input Lists

Informal description

For any natural numbers $b$ and $f$, and for any natural number $n$ and lists of characters $l_1$ and $l_2$, if the lengths of $l_1$ and $l_2$ are equal, then the lengths of the lists produced by `Nat.toDigitsCore b f n l1` and `Nat.toDigitsCore b f n l2` are also equal.

Nat.toDigitsCore_lens_eq theorem

 (b f : Nat) :
  ∀ (n : Nat) (c : Char) (tl : List Char),
    (Nat.toDigitsCore b f n (c :: tl)).length = (Nat.toDigitsCore b f n tl).length + 1

Full source

lemma toDigitsCore_lens_eq (b f : Nat) : ∀ (n : Nat) (c : Char) (tl : List Char),
    (Nat.toDigitsCore b f n (c :: tl)).length = (Nat.toDigitsCore b f n tl).length + 1 := by
  induction f with (intro n c tl; simp only [Nat.toDigitsCore, List.length])
  | succ f ih =>
    if hnb : (n / b) = 0 then
      simp only [hnb, if_true, List.length]
    else
      generalize hx : Nat.digitChar (n % b) = x
      simp only [hx, hnb, if_false] at ih
      simp only [hnb, if_false]
      specialize ih (n / b) c (x :: tl)
      rw [← ih]
      have lens_eq : (x :: (c :: tl)).length = (c :: x :: tl).length := by simp
      apply toDigitsCore_lens_eq_aux
      exact lens_eq

Length Increment in `Nat.toDigitsCore` When Prepending a Character

Informal description

For any natural numbers $b$ and $f$, any natural number $n$, any character $c$, and any list of characters $tl$, the length of the list produced by `Nat.toDigitsCore b f n (c :: tl)` is equal to the length of the list produced by `Nat.toDigitsCore b f n tl` plus one. In other words, prepending a character $c$ to the input list increases the output length by exactly one.

Nat.nat_repr_len_aux theorem

(n b e : Nat) (h_b_pos : 0 < b) : n < b ^ e.succ → n / b < b ^ e

Full source

lemma nat_repr_len_aux (n b e : Nat) (h_b_pos : 0 < b) :  n < b ^ e.succ → n / b < b ^ e := by
  simp only [Nat.pow_succ]
  exact (@Nat.div_lt_iff_lt_mul b n (b ^ e) h_b_pos).mpr

Divisibility Bound for Natural Numbers in Base $b$ Exponents

Informal description

For any natural numbers $n$, $b$, and $e$ with $b > 0$, if $n < b^{e+1}$, then the integer division $n / b$ satisfies $n / b < b^e$.

Nat.toDigitsCore_length theorem

(b f n e : Nat) (h_e_pos : 0 < e) (hlt : n < b ^ e) : (Nat.toDigitsCore b f n []).length ≤ e

Full source

/-- The String representation produced by toDigitsCore has the proper length relative to
the number of digits in `n < e` for some base `b`. Since this works with any base,
it can be used for binary, decimal, and hex. -/
lemma toDigitsCore_length (b f n e : Nat) (h_e_pos : 0 < e) (hlt : n < b ^ e) :
    (Nat.toDigitsCore b f n []).length ≤ e := by
  induction f generalizing n e hlt h_e_pos with
  | zero => simp only [toDigitsCore, List.length, zero_le]
  | succ f ih =>
    simp only [toDigitsCore]
    cases e with
    | zero => exact False.elim (Nat.lt_irrefl 0 h_e_pos)
    | succ e =>
      cases e with
      | zero =>
        rw [zero_add, pow_one] at hlt
        simp [Nat.div_eq_of_lt hlt]
      | succ e =>
        specialize ih (n / b) _ (add_one_pos e) (Nat.div_lt_of_lt_mul <| by rwa [← pow_add_one'])
        split_ifs
        · simp only [List.length_singleton, _root_.zero_le, succ_le_succ]
        · simp only [toDigitsCore_lens_eq b f (n / b) (Nat.digitChar <| n % b),
            Nat.succ_le_succ_iff, ih]

Bound on Length of `Nat.toDigitsCore` Output

Informal description

For any natural numbers $b$, $f$, $n$, and $e$ with $e > 0$, if $n < b^e$, then the length of the string representation produced by `Nat.toDigitsCore b f n []` is at most $e$.

Nat.toDigits_length theorem

(b n e : Nat) : 0 < e → n < b ^ e → (Nat.toDigits b n).length ≤ e

Full source

/-- The core implementation of `Nat.toDigits` returns a String with length less than or equal to the
number of digits in the base-`b` number (represented by `e`). For example, the string
representation of any number less than `b ^ 3` has a length less than or equal to 3. -/
lemma toDigits_length (b n e : Nat) : 0 < e → n < b ^ e → (Nat.toDigits b n).length ≤ e :=
  toDigitsCore_length _ _ _ _

Bound on Length of Base-$b$ Digit Representation: $\text{length}(\text{toDigits}(b, n)) \leq e$ when $n < b^e$

Informal description

For any natural numbers $b$, $n$, and $e$ with $e > 0$, if $n < b^e$, then the length of the string representation of $n$ in base $b$ (produced by `Nat.toDigits`) is at most $e$.

Nat.repr_length theorem

(n e : Nat) : 0 < e → n < 10 ^ e → (Nat.repr n).length ≤ e

Full source

/-- The core implementation of `Nat.repr` returns a String with length less than or equal to the
number of digits in the decimal number (represented by `e`). For example, the decimal string
representation of any number less than 1000 (10 ^ 3) has a length less than or equal to 3. -/
lemma repr_length (n e : Nat) : 0 < e → n < 10 ^ e → (Nat.repr n).length ≤ e :=
  toDigits_length _ _ _

Length Bound for Decimal String Representation: $\text{length}(\text{repr}(n)) \leq e$ when $n < 10^e$

Informal description

For any natural numbers $n$ and $e$ with $e > 0$, if $n < 10^e$, then the length of the decimal string representation of $n$ is at most $e$.

Nat.NormDigits.digits_succ theorem

 (b n m r l) (e : r + b * m = n) (hr : r < b) (h : Nat.digits b m = l ∧ 1 < b ∧ 0 < m) :
  (Nat.digits b n = r :: l) ∧ 1 < b ∧ 0 < n

Full source

theorem digits_succ (b n m r l) (e : r + b * m = n) (hr : r < b)
    (h : Nat.digitsNat.digits b m = l ∧ 1 < b ∧ 0 < m) : (Nat.digits b n = r :: l) ∧ 1 < b ∧ 0 < n := by
  rcases h with ⟨h, b2, m0⟩
  have b0 : 0 < b := by omega
  have n0 : 0 < n := by linarith [mul_pos b0 m0]
  refine ⟨?_, b2, n0⟩
  obtain ⟨rfl, rfl⟩ := (Nat.div_mod_unique b0).2 ⟨e, hr⟩
  subst h; exact Nat.digits_def' b2 n0

Recursive Digit Expansion in Base $b$: $\text{digits}_b(n) = r :: \text{digits}_b(m)$ when $n = r + b \cdot m$ and $r < b$

Informal description

Let $b$, $n$, $m$, $r$, and $l$ be natural numbers such that: 1. $r + b \cdot m = n$, 2. $r < b$, 3. The digits of $m$ in base $b$ are given by $l$ (i.e., $\text{digits}_b(m) = l$), 4. $b > 1$ and $m > 0$. Then the digits of $n$ in base $b$ are given by $r$ followed by $l$ (i.e., $\text{digits}_b(n) = r :: l$), and moreover $b > 1$ and $n > 0$.

Nat.NormDigits.digits_one theorem

(b n) (n0 : 0 < n) (nb : n < b) : Nat.digits b n = [n] ∧ 1 < b ∧ 0 < n

Full source

theorem digits_one (b n) (n0 : 0 < n) (nb : n < b) : Nat.digitsNat.digits b n = [n] ∧ 1 < b ∧ 0 < n := by
  have b2 : 1 < b :=
    lt_iff_add_one_le.mpr (le_trans (add_le_add_right (lt_iff_add_one_le.mp n0) 1) nb)
  refine ⟨?_, b2, n0⟩
  rw [Nat.digits_def' b2 n0, Nat.mod_eq_of_lt nb, Nat.div_eq_zero_iff.2 <| .inr nb, Nat.digits_zero]

Single-digit representation in base $b$ when $0 < n < b$

Informal description

For any natural numbers $b$ and $n$ such that $0 < n < b$, the digits of $n$ in base $b$ consist of the single-element list $[n]$, and moreover $b > 1$ and $n > 0$.

TODO