Theorems · Definition · number theory

Nat.digits

ℕ → ℕ → List ℕ

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 = [].

Defined in

Mathlib.Data.Nat.Digits.Defs

Cited by

70 results in Mathlib

Foundations

Depth 28 from the axioms · uses propext, Classical.choice, Quot.sound