Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-20 05:06 84d4ea77

View on Github →

feat(data/nat/digits): a bigger number has more digits (#3457)

Estimated changes

Modified src/data/nat/digits.lean

added theorem digits_len_le_digits_len_succ

added theorem digits_one

modified theorem digits_one_succ

added theorem digits_zero_succ

added theorem digits_zero_zero

added theorem le_digits_len_le