batteries icon indicating copy to clipboard operation
batteries copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat: add `Nat.Digits`

Open fgdorais opened this issue 5 months ago • 3 comments

This PR adds functions for calculating digit representation in any base. Both little-endian and big-endian versions are provided.

fgdorais avatar Jun 26 '25 17:06 fgdorais

You might want to consider that #799 ought to be compatible with this. I am sure there's a lemma like this in Mathlib somewhere but I can't find it.

linesthatinterlace avatar Sep 30 '25 08:09 linesthatinterlace

(Mathlib has Nat.bits, which modulo finTwoEquiv is the same as this.)

linesthatinterlace avatar Sep 30 '25 08:09 linesthatinterlace

Good reminders! This PR is on hiatus until I find time to rethink the overall design.

fgdorais avatar Sep 30 '25 12:09 fgdorais