Skip to content

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

Closed
joelriou wants to merge 33 commits intomasterfrom
port/Algebra.Homology.Homotopy
Closed

[Merged by Bors] - feat: port Algebra.Homology.Homotopy#3524
joelriou wants to merge 33 commits intomasterfrom
port/Algebra.Homology.Homotopy

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

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

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
@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
@joelriou joelriou removed the WIP Work in progress label Apr 19, 2023
@joelriou joelriou mentioned this pull request Apr 19, 2023
Closed
5 tasks
@kim-em kim-em removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label 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

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

@joelriou
Copy link
Copy Markdown
Contributor Author

joelriou commented Apr 19, 2023

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
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
@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
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.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
kim-em 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.

4 participants

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