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] - refactor(algebra/group_power, data/nat/basic): remove redundant lemmas #4243

Closed
wants to merge 6 commits into from
Closed

[Merged by Bors] - refactor(algebra/group_power, data/nat/basic): remove redundant lemmas #4243

wants to merge 6 commits into from

Commits on Sep 24, 2020

  1. wip: move lemmas to algebra.group_power.basic; protect nat versions

    @rwbarton
    rwbarton committed Sep 24, 2020
    Configuration menu
    Copy the full SHA
    36fe765 View commit details
    Browse the repository at this point in the history

  2. remove nat pow lemmas

    @rwbarton
    rwbarton committed Sep 24, 2020
    Configuration menu
    Copy the full SHA
    db0296f View commit details
    Browse the repository at this point in the history

  3. remove unnecessary _root_ disambiguations

    @rwbarton
    rwbarton committed Sep 24, 2020
    Configuration menu
    Copy the full SHA
    b8e5283 View commit details
    Browse the repository at this point in the history

  4. remove nat.pow_succ

    @rwbarton
    rwbarton committed Sep 24, 2020
    Configuration menu
    Copy the full SHA
    3f1a740 View commit details
    Browse the repository at this point in the history

  5. remove a TODO that is done

    @rwbarton
    rwbarton committed Sep 24, 2020
    Configuration menu
    Copy the full SHA
    fcd513e View commit details
    Browse the repository at this point in the history

  6. fix archive/

    @rwbarton
    rwbarton committed Sep 24, 2020
    Configuration menu
    Copy the full SHA
    15d3c49 View commit details
    Browse the repository at this point in the history