mathlib3

47f73356 - feat(data/nat/digits): digits, and divisibility tests for Freek 85 (#2686)

feat(data/nat/digits): digits, and divisibility tests for Freek 85 (#2686) I couldn't quite believe how much low hanging fruit there is on Lean's attempt at Freek's list, and so took a moment to do surely the lowest of the low... This provides `digits b n`, which extracts the digits of a natural number `n` with respect to a base `b`, and `of_digits b L`, which reconstitutes a number from its digits, proves a few simple facts about these functions, and proves the usual divisibility by 3, 9, and 11 tests. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>