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 Algebra.Homology.Homotopy #3524

Closed
wants to merge 33 commits into from
Closed

[Merged by Bors] - feat: port Algebra.Homology.Homotopy #3524

wants to merge 33 commits into from

Conversation

joelriou
Copy link
Collaborator

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

Parcly-Taxel and others added 30 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
fixed unused variables
882581c
@Parcly-Taxel
Merge branch 'master' into port/Algebra.Homology.Additive
e9e3ed9
@joelriou
feat: port Algebra.Homology.Homotopy
578b91b
@joelriou
Initial file copy from mathport
01ea19a
@joelriou
automated fixes
93abaa5 
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
@joelriou
Merge remote-tracking branch 'origin/port/Algebra.Homology.Additive' …
b379525 
…into port/Algebra.Homology.Homotopy
@joelriou joelriou added WIP Work in progress mathlib-port This is a port of a theory file from mathlib. labels Apr 19, 2023
@joelriou joelriou mentioned this pull request Apr 19, 2023
Closed
4 tasks
@semorrison semorrison added the blocked-by-other-PR This PR depends on another PR which is still in the queue. label Apr 19, 2023
@joelriou joelriou removed the WIP Work in progress label Apr 19, 2023
@joelriou joelriou mentioned this pull request Apr 19, 2023
Closed
5 tasks
@semorrison semorrison removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. label Apr 19, 2023
@semorrison
Copy link
Contributor

This PR/issue depends on:

@Parcly-Taxel Parcly-Taxel added the awaiting-review The author would like community review of the PR label Apr 19, 2023
@ChrisHughes24
Copy link
Member

There seem to have been some comments that were lost before the definition of fromNext and toPrev. Was this intentional?

@joelriou
Copy link
Collaborator Author

There seem to have been some comments that were lost before the definition of fromNext and toPrev. Was this intentional?

Indeed, it is intentional: these comments have become irrelevant because of a refactor that was done a few months ago.

@ChrisHughes24
Copy link
Member

bors r+

@github-actions github-actions bot 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 Apr 19, 2023
bors bot pushed a commit that referenced this pull request Apr 19, 2023
@joelriou @ChrisHughes24 @Parcly-Taxel
feat: port Algebra.Homology.Homotopy (#3524)
4f99e00 
Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
@bors
Copy link

bors bot commented Apr 19, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port Algebra.Homology.Homotopy [Merged by Bors] - feat: port Algebra.Homology.Homotopy Apr 19, 2023
@bors bors bot closed this Apr 19, 2023
@bors bors bot deleted the port/Algebra.Homology.Homotopy branch April 19, 2023 22:41
semorrison pushed a commit that referenced this pull request May 10, 2023
@joelriou @ChrisHughes24 @Parcly-Taxel
feat: port Algebra.Homology.Homotopy (#3524)
097302e 
Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ChrisHughes24 ChrisHughes24 Awaiting requested review from ChrisHughes24

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
4 participants
@joelriou @semorrison @ChrisHughes24 @Parcly-Taxel