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.

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

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

Closed
wants to merge 10 commits into from

Commits on Feb 20, 2023

  1. Configuration menu
    Copy the full SHA
    a2c9da6 View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    7fb21a3 View commit details
    Browse the repository at this point in the history
  3. automated fixes

    Mathbin -> Mathlib
    
    fix certain import statements
    
    move "by" to end of line
    
    add import to Mathlib.lean
    mattrobball committed Feb 20, 2023
    Configuration menu
    Copy the full SHA
    f6f3b75 View commit details
    Browse the repository at this point in the history
  4. :wqaSquashed commit of the following:

    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 committed Feb 20, 2023
    Configuration menu
    Copy the full SHA
    a388072 View commit details
    Browse the repository at this point in the history
  5. fix weird merge

    mattrobball committed Feb 20, 2023
    Configuration menu
    Copy the full SHA
    acc5394 View commit details
    Browse the repository at this point in the history
  6. fix errors; lint

    mattrobball committed Feb 20, 2023
    Configuration menu
    Copy the full SHA
    eb6a39e View commit details
    Browse the repository at this point in the history
  7. Configuration menu
    Copy the full SHA
    f4bbf9e View commit details
    Browse the repository at this point in the history
  8. fix borked import file

    3rd time = 🧿?
    mattrobball committed Feb 20, 2023
    Configuration menu
    Copy the full SHA
    658c05b View commit details
    Browse the repository at this point in the history

Commits on Feb 22, 2023

  1. add updated discrete cat

    mattrobball committed Feb 22, 2023
    Configuration menu
    Copy the full SHA
    97da3ee View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    8f0770b View commit details
    Browse the repository at this point in the history