Positional Notation for Natural Numbers in an Arbitrary Base

Charles Staats 📧

April 3, 2023

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: