Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

feat(data/*/quot): quotient_lift on a finite family#18315

Closed
astrainfinita wants to merge 22 commits intomasterfrom
FR_quotient2
Closed

feat(data/*/quot): quotient_lift on a finite family#18315
astrainfinita wants to merge 22 commits intomasterfrom
FR_quotient2

Conversation

@astrainfinita
Copy link
Copy Markdown
Collaborator

@astrainfinita astrainfinita commented Jan 27, 2023 •
edited by github-actions bot
Loading

@astrainfinita astrainfinita added RFC Request for comment awaiting-review The author would like community review of the PR awaiting-CI The author would like to see what CI has to say before doing more work. and removed RFC Request for comment labels Jan 27, 2023
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Jan 27, 2023
@astrainfinita astrainfinita mentioned this pull request Jan 27, 2023
Open
2 tasks
@alreadydone
Copy link
Copy Markdown
Collaborator

alreadydone commented Jan 29, 2023

Hi! Please check out my comment on Zulip if you haven't.

@astrainfinita astrainfinita mentioned this pull request Jan 30, 2023
Closed
@eric-wieser
Copy link
Copy Markdown
Member

eric-wieser commented Jan 31, 2023

I think this will be easier to port if we do #18337 first.

@ghost ghost added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Jan 31, 2023
@astrainfinita astrainfinita added the WIP Work in progress label Jan 31, 2023
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Feb 1, 2023
@eric-wieser
Copy link
Copy Markdown
Member

eric-wieser commented Feb 1, 2023

I renamed all the files to quotient since your results are all about quotient s not quot r, and resolved the merge conflicts. You should be able to merge this PR back into your other PR to propagate the changes, assuming you want to keep this.

@astrainfinita astrainfinita removed WIP Work in progress mathlib4-pair labels Feb 10, 2023
@astrainfinita astrainfinita added the awaiting-CI The author would like to see what CI has to say before doing more work. label Feb 10, 2023
@astrainfinita astrainfinita mentioned this pull request Feb 10, 2023
Closed
@ghost ghost added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Feb 10, 2023
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Feb 12, 2023
@Komyyy Komyyy mentioned this pull request May 14, 2023
Closed
@eric-wieser eric-wieser added the not-too-late This PR was ready at the point mathlib3 was frozen: we will try to merge it and port it to mathlib4 label Jul 15, 2023
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Jul 27, 2023
@ghost
Copy link
Copy Markdown

ghost commented Jul 27, 2023

This PR/issue depends on:

@astrainfinita
Copy link
Copy Markdown
Collaborator Author

astrainfinita commented Jul 28, 2023

Replaced by leanprover-community/mathlib4#5576.

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Reviewers

No reviews

Assignees

No one assigned

Labels

awaiting-review The author would like community review of the PR not-too-late This PR was ready at the point mathlib3 was frozen: we will try to merge it and port it to mathlib4

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@astrainfinita @alreadydone @eric-wieser