Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-27 00:02 ca6cebc5

View on Github →

feat(data/nat/digits): add last_digit_ne_zero (#3544) The proof of base_pow_length_digits_le was refactored as suggested by @fpvandoorn in #3498.

Estimated changes

added theorem list.last_repeat_succ
modified theorem base_pow_length_digits_le'
added theorem digits_last
added theorem last_digit_ne_zero
added theorem of_digits_singleton