Commit 2020-07-16 14:24 25be04ae

View on Github →

feat(data/nat/digits): add lemmas about digits (#3406) Added lt_base_pow_length_digits, of_digits_lt_base_pow_length, of_digits_append and of_digits_digits_append_digits

Estimated changes

Modified src/data/nat/digits.lean

added theorem lt_base_pow_length_digits'

added theorem lt_base_pow_length_digits

added theorem of_digits_append

added theorem of_digits_digits_append_digits

added theorem of_digits_lt_base_pow_length'

added theorem of_digits_lt_base_pow_length