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

feat(*): some simple lemmas about sets and finite sets #1903

Merged
merged 9 commits into from
Jan 26, 2020
Merged

feat(*): some simple lemmas about sets and finite sets #1903

merged 9 commits into from
Jan 26, 2020

Commits on Jan 25, 2020

  1. feat(*): some simple lemmas about sets and finite sets

    @urkud
    urkud committed Jan 25, 2020
    Configuration menu
    Copy the full SHA
    ed651fd View commit details
    Browse the repository at this point in the history

  2. More lemmas, simplify proofs

    @urkud
    urkud committed Jan 25, 2020
    Configuration menu
    Copy the full SHA
    be1afa3 View commit details
    Browse the repository at this point in the history

  3. Introduce finsup.nonempty and use it.

    @urkud
    urkud committed Jan 25, 2020
    Configuration menu
    Copy the full SHA
    9f05140 View commit details
    Browse the repository at this point in the history

  4. Update src/algebra/big_operators.lean 

    Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
    @urkud @ChrisHughes24
    urkud and ChrisHughes24 committed Jan 25, 2020
    Configuration menu
    Copy the full SHA
    17c89a8 View commit details
    Browse the repository at this point in the history

  5. Revert "Update src/algebra/big_operators.lean" 

    This reverts commit 17c89a8. It
breaks compile if we rewrite right to left.
    @urkud
    urkud committed Jan 25, 2020
    Configuration menu
    Copy the full SHA
    35a7589 View commit details
    Browse the repository at this point in the history

  6. simp, to_additive

    @urkud
    urkud committed Jan 25, 2020
    Configuration menu
    Copy the full SHA
    89431ee View commit details
    Browse the repository at this point in the history

  7. Merge branch 'master' into set-finset

    @urkud
    urkud committed Jan 25, 2020
    Configuration menu
    Copy the full SHA
    4d8743b View commit details
    Browse the repository at this point in the history

  8. Add a missing docstring

    @urkud
    urkud committed Jan 25, 2020
    Configuration menu
    Copy the full SHA
    ad43229 View commit details
    Browse the repository at this point in the history

  9. Merge branch 'master' into set-finset

    @mergify
    mergify[bot] committed Jan 25, 2020
    Configuration menu
    Copy the full SHA
    cd0fa53 View commit details
    Browse the repository at this point in the history