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.

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

[Merged by Bors] - feat: port AlgebraicTopology.DoldKan.NCompGamma #3576

Closed
wants to merge 39 commits into from

Conversation

Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
…egeneracies' into port/AlgebraicTopology.DoldKan.SplitSimplicialObject
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
…plitSimplicialObject' into port/AlgebraicTopology.DoldKan.FunctorGamma
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
…unctorGamma' into port/AlgebraicTopology.DoldKan.GammaCompN
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
…ammaCompN' into port/AlgebraicTopology.DoldKan.NCompGamma
@joelriou joelriou added WIP Work in progress mathlib-port This is a port of a theory file from mathlib. labels Apr 21, 2023
@semorrison semorrison added the blocked-by-other-PR This PR depends on another PR to Mathlib label Apr 21, 2023
…ammaCompN' into port/AlgebraicTopology.DoldKan.NCompGamma
@semorrison semorrison removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Apr 21, 2023
@joelriou joelriou removed the WIP Work in progress label Apr 21, 2023
@joelriou joelriou added the WIP Work in progress label Apr 22, 2023
@joelriou joelriou removed the WIP Work in progress label Apr 22, 2023
@semorrison semorrison removed the blocked-by-other-PR This PR depends on another PR to Mathlib label Apr 22, 2023
@joelriou joelriou added the awaiting-review The author would like community review of the PR label Apr 22, 2023
@semorrison
Copy link
Contributor

Thanks, @joelriou. It's a bit worrying that we're seeing more timeouts here, although it may well be that we're just operating within stricter limits now --- as far as I know no one has attempted to compare the (incomparable?) different limits in mathlib3 and mathlib4.

In any case, adding irreducible is a positive step, rather than a regression!

bors merge

@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 22, 2023
bors bot pushed a commit that referenced this pull request Apr 22, 2023
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@bors
Copy link

bors bot commented Apr 23, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port AlgebraicTopology.DoldKan.NCompGamma [Merged by Bors] - feat: port AlgebraicTopology.DoldKan.NCompGamma Apr 23, 2023
@bors bors bot closed this Apr 23, 2023
@bors bors bot deleted the port/AlgebraicTopology.DoldKan.NCompGamma branch April 23, 2023 00:19
semorrison added a commit that referenced this pull request May 10, 2023
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
hrmacbeth pushed a commit that referenced this pull request May 10, 2023
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
hrmacbeth pushed a commit that referenced this pull request May 11, 2023
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
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
Development

Successfully merging this pull request may close these issues.

None yet

3 participants