Commit 2022-01-06 07:55 69521729
View on Github →feat(data/nat/digits): digits_len (#11187)
Via a new data.nat.log import.
Also unprivate digits_eq_cons_digits_div.
The file needs a refactor to make the names more mathlib-like,
otherwise I would have named it length_digits.