PR #7813 feat(data/nat/digits): Add lemmas

feat(data/nat/digits): Add lemmas #7813

Pazzaz wants to merge 7 commits into master from digits_prefix

Add various lemmas about digits

17e3c55a

Add docs for `digits_of_digits_prefix`

7ef8d837

Remove unnecessary lemmas

0ec0b501

eric-wieser commented on 2021-06-03

Remove a hypothesis from`digits_of_digits_prefix`

7e644e54

eric-wieser commented on 2021-06-04

Remove space

70d5a9ee

eric-wieser approved these changes on 2021-06-04

eric-wieser added awaiting-review

ericrbg approved these changes on 2021-06-04

Small changes

02b0d234

Merge branch 'digits_prefix' of https://github.com/leanprover-communi…

09a8a09e

kim-em commented on 2021-06-07

jcommelin removed awaiting-review

jcommelin added awaiting-author

kim-em added too-late

Reviewers

ericrbg

eric-wieser

kim-em

Assignees

No one assigned

Labels

awaiting-author too-late

Milestone

No milestone