Positional Notation for Natural Numbers in an Arbitrary Base

Charles Staats 📧

April 3, 2023

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


We demonstrate the existence and uniqueness of the base-$n$ representation of a natural number, where $n$ is any natural number greater than 1. This comes up when trying to translate mathematical contest problems and solutions into Isabelle/HOL.


BSD License


Session DigitsInBase