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: port CategoryTheory.IsomorphismClasses #2394

Closed
wants to merge 10 commits into from
Closed

[Merged by Bors] - feat: port CategoryTheory.IsomorphismClasses #2394

wants to merge 10 commits into from

Conversation

mattrobball
Copy link
Collaborator

@mattrobball mattrobball commented Feb 20, 2023 •
edited

@mattrobball
feat: port CategoryTheory.IsomorphismClasses
a2c9da6
@mattrobball
Initial file copy from mathport
7fb21a3
@mattrobball
automated fixes
f6f3b75 
Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean
@mattrobball
:wqaSquashed commit of the following:
a388072 
commit 8f68883
Merge: 405cecc eab0a09
Author: Matthew Ballard <matt@mrb.email>
Date:   Mon Feb 20 09:37:07 2023 -0500

    Merge branch 'master' into port/CategoryTheory.Category.Cat

commit 405cecc
Author: Matthew Ballard <matt@mrb.email>
Date:   Sun Feb 19 08:48:18 2023 -0500

    fix errors; lint

commit 25b7383
Author: Matthew Ballard <matt@mrb.email>
Date:   Sun Feb 19 08:11:21 2023 -0500

    remove script

commit dfa581d
Author: Matthew Ballard <matt@mrb.email>
Date:   Sun Feb 19 08:10:44 2023 -0500

    Squashed commit of the following:

    commit 24c70cb
    Merge: 38a89b8 18f8822
    Author: Matthew Ballard <matt@mrb.email>
    Date:   Thu Feb 16 20:20:59 2023 -0500

        Merge remote-tracking branch 'refs/remotes/origin/port/CategoryTheory.DiscreteCategory' into port/CategoryTheory.DiscreteCategory

    commit 38a89b8
    Author: Matthew Ballard <matt@mrb.email>
    Date:   Thu Feb 16 20:20:24 2023 -0500

        lint some more

    commit 18f8822
    Merge: eb14644 68e722a
    Author: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com>
    Date:   Thu Feb 16 20:16:53 2023 -0500

        Merge branch 'master' into port/CategoryTheory.DiscreteCategory

    commit eb14644
    Author: Matthew Ballard <matt@mrb.email>
    Date:   Thu Feb 16 20:14:21 2023 -0500

        lint

    commit 8860e0d
    Author: adamtopaz <github@adamtopaz.com>
    Date:   Thu Feb 16 17:33:00 2023 -0700

        get file to build

    commit 2203485
    Author: adamtopaz <github@adamtopaz.com>
    Date:   Tue Feb 14 22:06:54 2023 -0700

        automated fixes

        Mathbin -> Mathlib

        fix certain import statements

        move "by" to end of line

        add import to Mathlib.lean

    commit 10bf4bb
    Author: adamtopaz <github@adamtopaz.com>
    Date:   Tue Feb 14 22:06:54 2023 -0700

        Initial file copy from mathport

    commit 82e2512
    Author: adamtopaz <github@adamtopaz.com>
    Date:   Tue Feb 14 22:06:54 2023 -0700

        feat: port CategoryTheory.DiscreteCategory

commit 64556c5
Author: Matthew Ballard <matt@mrb.email>
Date:   Sun Feb 19 08:08:19 2023 -0500

    automated fixes

    Mathbin -> Mathlib

    fix certain import statements

    move "by" to end of line

    add import to Mathlib.lean

commit e14a0f5
Author: Matthew Ballard <matt@mrb.email>
Date:   Sun Feb 19 08:08:19 2023 -0500

    Initial file copy from mathport

commit 967e14a
Author: Matthew Ballard <matt@mrb.email>
Date:   Sun Feb 19 08:08:19 2023 -0500

    feat: port CategoryTheory.Category.Cat
@mattrobball
fix weird merge
acc5394
@mattrobball
fix errors; lint
eb6a39e
@mattrobball mattrobball added the mathlib-port This is a port of a theory file from mathlib. label Feb 20, 2023
@semorrison semorrison added blocked-by-other-PR This PR depends on another PR which is still in the queue. merge-conflict The PR has a merge conflict with master, and needs manual merging. labels Feb 20, 2023
@mattrobball mattrobball mentioned this pull request Feb 22, 2023
Closed
1 task
@semorrison semorrison removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. label Feb 22, 2023
@semorrison
Copy link
Contributor

This PR/issue depends on:

@semorrison semorrison removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Feb 22, 2023
@mattrobball mattrobball added the awaiting-review The author would like community review of the PR label Feb 22, 2023
jcommelin
jcommelin approved these changes Feb 22, 2023
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks 🎉

bors merge

@semorrison semorrison added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Feb 22, 2023
bors bot pushed a commit that referenced this pull request Feb 22, 2023
@mattrobball
feat: port CategoryTheory.IsomorphismClasses (#2394)
b2dca69
@bors
Copy link

bors bot commented Feb 22, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port CategoryTheory.IsomorphismClasses [Merged by Bors] - feat: port CategoryTheory.IsomorphismClasses Feb 22, 2023
@bors bors bot closed this Feb 22, 2023
@bors bors bot deleted the port/CategoryTheory.IsomorphismClasses branch February 22, 2023 04:23
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jcommelin jcommelin jcommelin approved these changes

Assignees
No one assigned
Labels
mathlib-port This is a port of a theory file from mathlib. ready-to-merge This PR has been sent to bors.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@mattrobball @semorrison @jcommelin