Skip to content

[Merged by Bors] - feat: port AlgebraicTopology.DoldKan.Faces#3526

Closed
joelriou wants to merge 60 commits intomasterfrom
port/AlgebraicTopology.DoldKan.Faces
Closed

[Merged by Bors] - feat: port AlgebraicTopology.DoldKan.Faces#3526
joelriou wants to merge 60 commits intomasterfrom
port/AlgebraicTopology.DoldKan.Faces

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
@joelriou
feat: port AlgebraicTopology.AlternatingFaceMapComplex
505754f
@joelriou
Initial file copy from mathport
30b5fb3
@joelriou
automated fixes
52fed29 
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' …
d5903d7 
…into port/AlgebraicTopology.AlternatingFaceMapComplex
@joelriou
it compiles
a0edcc8
@kim-em kim-em added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 19, 2023
@kim-em kim-em removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 19, 2023
@joelriou joelriou removed the WIP Work in progress label Apr 19, 2023
@Parcly-Taxel Parcly-Taxel removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Apr 20, 2023
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Apr 20, 2023

This PR/issue depends on:

This was referenced Apr 20, 2023
Closed
Closed
Closed
Closed
Closed
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Apr 20, 2023

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Apr 20, 2023
bors bot pushed a commit that referenced this pull request Apr 20, 2023
@Parcly-Taxel @joelriou
feat: port AlgebraicTopology.DoldKan.Faces (#3526)
ff636cc 
Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
@bors
Copy link
Copy Markdown

bors bot commented Apr 20, 2023

This PR was included in a batch that was canceled, it will be automatically retried

bors bot pushed a commit that referenced this pull request Apr 20, 2023
@Parcly-Taxel @joelriou
feat: port AlgebraicTopology.DoldKan.Faces (#3526)
c086651 
Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
@joelriou joelriou mentioned this pull request Apr 20, 2023
Closed
4 tasks
@bors
Copy link
Copy Markdown

bors bot commented Apr 20, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port AlgebraicTopology.DoldKan.Faces [Merged by Bors] - feat: port AlgebraicTopology.DoldKan.Faces Apr 20, 2023
@bors bors bot closed this Apr 20, 2023
@bors bors bot deleted the port/AlgebraicTopology.DoldKan.Faces branch April 20, 2023 11:28
kbuzzard pushed a commit that referenced this pull request Apr 22, 2023
@Parcly-Taxel @joelriou @kbuzzard
feat: port AlgebraicTopology.DoldKan.Faces (#3526)
7454868 
Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
kim-em pushed a commit that referenced this pull request May 10, 2023
@Parcly-Taxel @joelriou
feat: port AlgebraicTopology.DoldKan.Faces (#3526)
a832353 
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.

3 participants

@joelriou @kim-em @Parcly-Taxel