Skip to content

[Merged by Bors] - feat: port AlgebraicTopology.DoldKan.HomotopyEquivalence#3594

Closed
joelriou wants to merge 12 commits intomasterfrom
port/AlgebraicTopology.DoldKan.HomotopyEquivalence
Closed

[Merged by Bors] - feat: port AlgebraicTopology.DoldKan.HomotopyEquivalence#3594
joelriou wants to merge 12 commits intomasterfrom
port/AlgebraicTopology.DoldKan.HomotopyEquivalence

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

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

joelriou added 9 commits April 22, 2023 14:57
@joelriou
feat: port AlgebraicTopology.DoldKan.Normalized
69886e3
@joelriou
Initial file copy from mathport
570cede
@joelriou
automated fixes
b5d23ec 
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
@joelriou
it compiles
ff6c1ba
@joelriou
fixed long line
8b2219d
@joelriou
feat: port AlgebraicTopology.DoldKan.HomotopyEquivalence
862af31
@joelriou
Initial file copy from mathport
16cd415
@joelriou
automated fixes
0c518c4 
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
@joelriou
Merge remote-tracking branch 'origin/port/AlgebraicTopology.DoldKan.N…
2603cf7 
…ormalized' into port/AlgebraicTopology.DoldKan.HomotopyEquivalence
@joelriou joelriou added WIP Work in progress mathlib-port This is a port of a theory file from mathlib. labels Apr 22, 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 22, 2023
@joelriou joelriou removed the WIP Work in progress label Apr 22, 2023
@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 23, 2023
@kim-em kim-em removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Apr 23, 2023
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Apr 24, 2023

This PR/issue depends on:

@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Apr 24, 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 24, 2023
bors bot pushed a commit that referenced this pull request Apr 24, 2023
@joelriou
feat: port AlgebraicTopology.DoldKan.HomotopyEquivalence (#3594)
f339c7d
@bors
Copy link
Copy Markdown

bors bot commented Apr 24, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port AlgebraicTopology.DoldKan.HomotopyEquivalence [Merged by Bors] - feat: port AlgebraicTopology.DoldKan.HomotopyEquivalence Apr 24, 2023
@bors bors bot closed this Apr 24, 2023
@bors bors bot deleted the port/AlgebraicTopology.DoldKan.HomotopyEquivalence branch April 24, 2023 12:12
kim-em pushed a commit that referenced this pull request May 10, 2023
@joelriou
feat: port AlgebraicTopology.DoldKan.HomotopyEquivalence (#3594)
450fc21
hrmacbeth pushed a commit that referenced this pull request May 10, 2023
@joelriou @hrmacbeth
feat: port AlgebraicTopology.DoldKan.HomotopyEquivalence (#3594)
2becc24
hrmacbeth pushed a commit that referenced this pull request May 11, 2023
@joelriou @hrmacbeth
feat: port AlgebraicTopology.DoldKan.HomotopyEquivalence (#3594)
1c23654
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.

2 participants

@joelriou @kim-em