Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat(data/nat/digits): add lemmas about digits #3406

Closed
wants to merge 4 commits into from
Closed

[Merged by Bors] - feat(data/nat/digits): add lemmas about digits #3406

wants to merge 4 commits into from

Commits on Jul 15, 2020

  1. feat(data/nat/digits): add lemmas about digits

    @shingtaklam1324
    shingtaklam1324 committed Jul 15, 2020
    Configuration menu
    Copy the full SHA
    df095b9 View commit details
    Browse the repository at this point in the history

  2. added of_digits_digits_append_digits

    @shingtaklam1324
    shingtaklam1324 committed Jul 15, 2020
    Configuration menu
    Copy the full SHA
    a64fa6d View commit details
    Browse the repository at this point in the history

  3. Update src/data/nat/digits.lean - remove extra whitespace 

    Co-authored-by: Johan Commelin <johan@commelin.net>
    @shingtaklam1324 @jcommelin
    shingtaklam1324 and jcommelin committed Jul 15, 2020
    Configuration menu
    Copy the full SHA
    0b17c43 View commit details
    Browse the repository at this point in the history

Commits on Jul 16, 2020

  1. changed len to length

    @shingtaklam1324
    shingtaklam1324 committed Jul 16, 2020
    Configuration menu
    Copy the full SHA
    840319c View commit details
    Browse the repository at this point in the history