Skip to content

[Merged by Bors] - feat: port CategoryTheory.Preadditive.Opposite#3505

Closed
joelriou wants to merge 19 commits intomasterfrom
port/CategoryTheory.Preadditive.Opposite
Closed

[Merged by Bors] - feat: port CategoryTheory.Preadditive.Opposite#3505
joelriou wants to merge 19 commits intomasterfrom
port/CategoryTheory.Preadditive.Opposite

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Apr 18, 2023 •
edited by Parcly-Taxel
Loading

Parcly-Taxel and others added 15 commits March 31, 2023 23:05
@Parcly-Taxel
feat: port Logic.Equiv.TransferInstance
f783d8e
@Parcly-Taxel
Initial file copy from mathport
058402d
@Parcly-Taxel
automated fixes
b062e98 
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
@Parcly-Taxel
23 problems
5f57a6e
@Parcly-Taxel
15 errors
18608bd
@Parcly-Taxel
7 errors, all simp
c787dba
@Parcly-Taxel
6 errors
5381819
@joelriou
Merge remote-tracking branch 'origin' into port/Logic.Equiv.TransferI…
36cc29a 
…nstance
@joelriou
it compiles
731bce0
@joelriou
removed import to LibrarySearch
41e78b0
@joelriou
some proof improvement
f77b5fa
@joelriou
feat: port CategoryTheory.Preadditive.Opposite
e2a97f6
@joelriou
Initial file copy from mathport
4bec176
@joelriou
automated fixes
b3fef04 
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
@joelriou
Merge remote-tracking branch 'origin/port/Logic.Equiv.TransferInstanc…
2e0adf8 
…e' into port/CategoryTheory.Preadditive.Opposite
@joelriou joelriou added WIP Work in progress mathlib-port This is a port of a theory file from mathlib. labels Apr 18, 2023
@kim-em kim-em added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Apr 18, 2023
@joelriou joelriou removed the WIP Work in progress label Apr 18, 2023
This was referenced Apr 19, 2023
Closed
Closed
@Parcly-Taxel Parcly-Taxel added awaiting-review and removed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Apr 19, 2023
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Apr 19, 2023

This PR/issue depends on:

This was referenced Apr 19, 2023
Closed
Closed
@joelriou joelriou mentioned this pull request Apr 19, 2023
Closed
2 tasks
@ChrisHughes24
Copy link
Copy Markdown
Member

ChrisHughes24 commented Apr 19, 2023

bors r+

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Apr 19, 2023
bors bot pushed a commit that referenced this pull request Apr 19, 2023
@Parcly-Taxel @joelriou
feat: port CategoryTheory.Preadditive.Opposite (#3505)
aea85a2 
Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
@joelriou joelriou mentioned this pull request Apr 19, 2023
Closed
5 tasks
@bors
Copy link
Copy Markdown

bors bot commented Apr 19, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port CategoryTheory.Preadditive.Opposite [Merged by Bors] - feat: port CategoryTheory.Preadditive.Opposite Apr 19, 2023
@bors bors bot closed this Apr 19, 2023
@bors bors bot deleted the port/CategoryTheory.Preadditive.Opposite branch April 19, 2023 13:42
kim-em pushed a commit that referenced this pull request May 10, 2023
@Parcly-Taxel @joelriou
feat: port CategoryTheory.Preadditive.Opposite (#3505)
8784a44 
Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

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.

4 participants

@joelriou @kim-em @ChrisHughes24 @Parcly-Taxel