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

[Merged by Bors] - chore(algebra/ring_quot): link ring_quot.rel with ring_con_gen #17892

Closed
wants to merge 18 commits into from
Closed

[Merged by Bors] - chore(algebra/ring_quot): link ring_quot.rel with ring_con_gen #17892

wants to merge 18 commits into from

Conversation

eric-wieser
Copy link
Member

@eric-wieser eric-wieser commented Dec 10, 2022 •
edited by github-actions bot
Loading

It's not clear to me whether it's worth keeping ring_quot.rel r around, or if it would be better to replace it entirely with ring_con_gen.

Open in Gitpod

@eric-wieser eric-wieser added WIP Work in progress RFC Request for comment awaiting-CI The author would like to see what CI has to say before doing more work. labels Dec 10, 2022
@eric-wieser eric-wieser requested a review from kim-em December 10, 2022 15:37
@eric-wieser eric-wieser added RFC Request for comment awaiting-review The author would like community review of the PR and removed RFC Request for comment WIP Work in progress labels Dec 10, 2022
@mathlib-dependent-issues-bot mathlib-dependent-issues-bot 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 Dec 10, 2022
@bors bors bot changed the base branch from eric-wieser/ring_con to master December 22, 2022 21:37
@mathlib-dependent-issues-bot mathlib-dependent-issues-bot 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 Dec 22, 2022
@mathlib-dependent-issues-bot
Copy link
Collaborator

This PR/issue depends on:

@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 Mar 15, 2023
YaelDillies
YaelDillies approved these changes Apr 1, 2023
View reviewed changes
Copy link
Collaborator

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Even if we get rid of ring_quot.rel, it is important that we can refer back to the link between the two definitions.

maintainer merge

@github-actions
Copy link

github-actions bot commented Apr 1, 2023

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

@ocfnash
Copy link
Collaborator

ocfnash commented Apr 2, 2023

Thanks!

bors merge

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Apr 2, 2023
bors bot pushed a commit that referenced this pull request Apr 2, 2023
@eric-wieser
chore(algebra/ring_quot): link ring_quot.rel with ring_con_gen (#17892)
e5820f6 
It's not clear to me whether it's worth keeping `ring_quot.rel r` around, or if it would be better to replace it entirely with `ring_con_gen`.
@bors
Copy link

bors bot commented Apr 2, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore(algebra/ring_quot): link ring_quot.rel with ring_con_gen [Merged by Bors] - chore(algebra/ring_quot): link ring_quot.rel with ring_con_gen Apr 2, 2023
@bors bors bot closed this Apr 2, 2023
@bors bors bot deleted the eric-wieser/ring_con-ring_quot branch April 2, 2023 19:50
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@YaelDillies YaelDillies YaelDillies approved these changes

@kim-em kim-em Awaiting requested review from kim-em

Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) RFC Request for comment
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@eric-wieser @mathlib-dependent-issues-bot @ocfnash @YaelDillies