-
Notifications
You must be signed in to change notification settings - Fork 263
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.PEmpty #2363
Closed
Closed
Commits on Feb 15, 2023
-
Configuration menu - View commit details
-
Copy full SHA for 82e2512 - Browse repository at this point
Copy the full SHA 82e2512View commit details -
Configuration menu - View commit details
-
Copy full SHA for 10bf4bb - Browse repository at this point
Copy the full SHA 10bf4bbView commit details -
Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean
Configuration menu - View commit details
-
Copy full SHA for 2203485 - Browse repository at this point
Copy the full SHA 2203485View commit details
Commits on Feb 17, 2023
-
Configuration menu - View commit details
-
Copy full SHA for 8860e0d - Browse repository at this point
Copy the full SHA 8860e0dView commit details -
Configuration menu - View commit details
-
Copy full SHA for eb14644 - Browse repository at this point
Copy the full SHA eb14644View commit details -
Configuration menu - View commit details
-
Copy full SHA for 18f8822 - Browse repository at this point
Copy the full SHA 18f8822View commit details -
Configuration menu - View commit details
-
Copy full SHA for 38a89b8 - Browse repository at this point
Copy the full SHA 38a89b8View commit details -
Merge remote-tracking branch 'refs/remotes/origin/port/CategoryTheory…
….DiscreteCategory' into port/CategoryTheory.DiscreteCategory
Configuration menu - View commit details
-
Copy full SHA for 24c70cb - Browse repository at this point
Copy the full SHA 24c70cbView commit details
Commits on Feb 18, 2023
-
Configuration menu - View commit details
-
Copy full SHA for 89d269b - Browse repository at this point
Copy the full SHA 89d269bView commit details -
Configuration menu - View commit details
-
Copy full SHA for 116924e - Browse repository at this point
Copy the full SHA 116924eView commit details -
Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean
Configuration menu - View commit details
-
Copy full SHA for 8f26549 - Browse repository at this point
Copy the full SHA 8f26549View commit details -
Configuration menu - View commit details
-
Copy full SHA for 740e069 - Browse repository at this point
Copy the full SHA 740e069View commit details -
Configuration menu - View commit details
-
Copy full SHA for 6fc9d77 - Browse repository at this point
Copy the full SHA 6fc9d77View commit details -
Configuration menu - View commit details
-
Copy full SHA for 89f4cac - Browse repository at this point
Copy the full SHA 89f4cacView commit details
Commits on Feb 21, 2023
-
Configuration menu - View commit details
-
Copy full SHA for a913c8d - Browse repository at this point
Copy the full SHA a913c8dView commit details -
Configuration menu - View commit details
-
Copy full SHA for 9bf1cef - Browse repository at this point
Copy the full SHA 9bf1cefView commit details -
Configuration menu - View commit details
-
Copy full SHA for 53d332a - Browse repository at this point
Copy the full SHA 53d332aView commit details -
Configuration menu - View commit details
-
Copy full SHA for 8d97fa3 - Browse repository at this point
Copy the full SHA 8d97fa3View commit details -
Configuration menu - View commit details
-
Copy full SHA for ebe5c7a - Browse repository at this point
Copy the full SHA ebe5c7aView commit details
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.