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: Better lemmas for transferring finite sums along equivalences #9237

Closed
wants to merge 14 commits into from
Closed

[Merged by Bors] - feat: Better lemmas for transferring finite sums along equivalences #9237

wants to merge 14 commits into from

Commits on Dec 23, 2023

  1. feat: Better lemmas for transferring finite sums along equivalences 

    Lemmas around this were a mess, throth in terms of names, statement and location. This PR standardises everything to be in `Algebra.BigOperators.Basic` and changes the lemmas to take in `InjOn` and `SurjOn` assumptions where possible (and where impossible make sure the hypotheses are taken in the correct order) and moves the equality of functions hypothesis last.

Also add a few lemma that help fix downstream uses by golfing.
    @YaelDillies
    YaelDillies committed Dec 23, 2023
    Configuration menu
    Copy the full SHA
    fb87f16 View commit details
    Browse the repository at this point in the history

  2. style 

    Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
    @YaelDillies @github-actions
    YaelDillies and github-actions[bot] committed Dec 23, 2023
    Configuration menu
    Copy the full SHA
    cda5688 View commit details
    Browse the repository at this point in the history

  3. fix

    @YaelDillies
    YaelDillies committed Dec 23, 2023
    Configuration menu
    Copy the full SHA
    dfc9bd1 View commit details
    Browse the repository at this point in the history

  4. fix

    @YaelDillies
    YaelDillies committed Dec 23, 2023
    Configuration menu
    Copy the full SHA
    267465a View commit details
    Browse the repository at this point in the history

  5. fix

    @YaelDillies
    YaelDillies committed Dec 23, 2023
    Configuration menu
    Copy the full SHA
    a7371c4 View commit details
    Browse the repository at this point in the history

Commits on Dec 26, 2023

  1. fix

    @YaelDillies
    YaelDillies committed Dec 26, 2023
    Configuration menu
    Copy the full SHA
    7adc36e View commit details
    Browse the repository at this point in the history

  2. fix

    @YaelDillies
    YaelDillies committed Dec 26, 2023
    Configuration menu
    Copy the full SHA
    d8f888a View commit details
    Browse the repository at this point in the history

  3. nits

    @YaelDillies
    YaelDillies committed Dec 26, 2023
    Configuration menu
    Copy the full SHA
    043baf1 View commit details
    Browse the repository at this point in the history

  4. Merge remote-tracking branch 'origin/master' into sum_bij

    @YaelDillies
    YaelDillies committed Dec 26, 2023
    Configuration menu
    Copy the full SHA
    837b37b View commit details
    Browse the repository at this point in the history

  5. fix

    @YaelDillies
    YaelDillies committed Dec 26, 2023
    Configuration menu
    Copy the full SHA
    a575ab4 View commit details
    Browse the repository at this point in the history

Commits on Dec 27, 2023

  1. fix Data.Set.Card

    @YaelDillies
    YaelDillies committed Dec 27, 2023
    Configuration menu
    Copy the full SHA
    4c1a276 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/master' into sum_bij

    @YaelDillies
    YaelDillies committed Dec 27, 2023
    Configuration menu
    Copy the full SHA
    2089370 View commit details
    Browse the repository at this point in the history

  3. docstrings

    @YaelDillies
    YaelDillies committed Dec 27, 2023
    Configuration menu
    Copy the full SHA
    2d4df14 View commit details
    Browse the repository at this point in the history

  4. fix

    @YaelDillies
    YaelDillies committed Dec 27, 2023
    Configuration menu
    Copy the full SHA
    fbfcac8 View commit details
    Browse the repository at this point in the history