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.

Abstract

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.

License

BSD License

Topics

Session DigitsInBase

Cite

× 
@article{DigitsInBase-AFP,
  author  = {Charles Staats},
  title   = {Positional Notation for Natural Numbers in an Arbitrary Base},
  journal = {Archive of Formal Proofs},
  month   = {April},
  year    = {2023},
  note    = {\url{https://isa-afp.org/entries/DigitsInBase.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: