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/Fintype/Basic): Finset.univ_map_subtype lemmas #12903

Closed
wants to merge 5 commits into from
Closed

[Merged by Bors] - feat(Data/Fintype/Basic): Finset.univ_map_subtype lemmas #12903

wants to merge 5 commits into from

Commits on May 14, 2024

  1. feat(Data/Fintype/Basic): Finset.univ_map_subtype lemmas

    @madvorak
    madvorak committed May 14, 2024
    Configuration menu
    Copy the full SHA
    e871996 View commit details
    Browse the repository at this point in the history

  2. Update Mathlib/Data/Fintype/Basic.lean 

    Co-authored-by: Richard Osborn <richardosborn@mac.com>
    @madvorak @rosborn
    madvorak and rosborn authored May 14, 2024
    Configuration menu
    Copy the full SHA
    7bfe50c View commit details
    Browse the repository at this point in the history

  3. rename according to rosborn and bugfix

    @madvorak
    madvorak committed May 14, 2024
    Configuration menu
    Copy the full SHA
    751d907 View commit details
    Browse the repository at this point in the history

Commits on Jun 12, 2024

  1. Update Mathlib/Data/Fintype/Basic.lean 

    Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
    @madvorak @Ruben-VandeVelde
    madvorak and Ruben-VandeVelde authored Jun 12, 2024
    Configuration menu
    Copy the full SHA
    541ad58 View commit details
    Browse the repository at this point in the history

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

    …type_filter
    @madvorak
    madvorak committed Jun 12, 2024
    Configuration menu
    Copy the full SHA
    41a8ebe View commit details
    Browse the repository at this point in the history