Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2020-07-22 16:16
a8cedf9f
View on Github →
feat(data/nat/digits): a number is bigger than base^(digits length - 1) (
#3498
)
Estimated changes
Modified
src/data/nat/digits.lean
added
theorem
base_pow_length_digits_le'
added
theorem
base_pow_length_digits_le