mathlib

69521729 - feat(data/nat/digits): digits_len (#11187)

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`.