Skip to content

[Merged by Bors] - feat: port Algebra.Homology.Additive#3517

Closed
joelriou wants to merge 26 commits intomasterfrom
port/Algebra.Homology.Additive
Closed

[Merged by Bors] - feat: port Algebra.Homology.Additive#3517
joelriou wants to merge 26 commits intomasterfrom
port/Algebra.Homology.Additive

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Apr 19, 2023 •
edited by github-actions bot
Loading

(Note: I mistakenly merged this with #3206 and #3505. Then, we should wait these two PRs are merged...)

Open in Gitpod

Parcly-Taxel and others added 24 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
it compiles
e66c33c
@joelriou
changed div_def/pow_def to match notation
0aa09f2
@joelriou
Merge remote-tracking branch 'origin/port/Logic.Equiv.TransferInstanc…
88903d3 
…e' into port/CategoryTheory.Preadditive.Opposite
@joelriou
feat: port Algebra.Homology.Additive
2759f8e
@joelriou
Initial file copy from mathport
c340cf6
@joelriou
automated fixes
f31c015 
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
@joelriou
Merge remote-tracking branch 'origin/port/CategoryTheory.Preadditive.…
116fa9e 
…Opposite' into port/Algebra.Homology.Additive
@joelriou
started working on this file
16ac588
@joelriou
it compiles
8079f28
@joelriou joelriou added the mathlib-port This is a port of a theory file from mathlib. label Apr 19, 2023
@joelriou joelriou changed the title feat: port Algebra.homology.additive feat: port Algebra.Homology.Additive Apr 19, 2023
@joelriou joelriou mentioned this pull request Apr 19, 2023
Closed
3 tasks
@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 19, 2023
@Parcly-Taxel
Copy link
Copy Markdown
Collaborator

Parcly-Taxel commented Apr 19, 2023

(Note: I mistakenly merged this with #3206 and #3505. Then, we should wait these two PRs are merged...)

Why not just close this PR, delete the branch and make a new branch/PR with just the Algebra.Homology.Additive file?

@joelriou
Copy link
Copy Markdown
Contributor Author

joelriou commented Apr 19, 2023

Why not just close this PR, delete the branch and make a new branch/PR with just the Algebra.Homology.Additive file?

Of course, I could have done this. But #3206 is already ready to merge :) and #3505 is straightforward, so that it is not causing a serious delay anyway.

This was referenced Apr 19, 2023
Closed
Closed
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:

@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 Algebra.Homology.Additive (#3517)
b1e0bf7 
Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
@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 Algebra.Homology.Additive [Merged by Bors] - feat: port Algebra.Homology.Additive Apr 19, 2023
@bors bors bot closed this Apr 19, 2023
kim-em pushed a commit that referenced this pull request May 10, 2023
@Parcly-Taxel @joelriou
feat: port Algebra.Homology.Additive (#3517)
3c2d274 
Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
@int-y1 int-y1 deleted the port/Algebra.Homology.Additive branch July 1, 2023 21:48
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 @Parcly-Taxel @kim-em @ChrisHughes24