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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat: Missing transfer instances #1725

Closed
wants to merge 3 commits into from
Closed

[Merged by Bors] - feat: Missing transfer instances #1725

wants to merge 3 commits into from

Conversation

YaelDillies
Copy link
Collaborator

@YaelDillies YaelDillies added the mathlib3-pair This PR is a forward-port of a mathlib3 PR or part of one, either under review or recently merged label Jan 20, 2023
@YaelDillies YaelDillies mentioned this pull request Jan 20, 2023
Closed
@YaelDillies YaelDillies added the awaiting-review The author would like community review of the PR label Jan 22, 2023
@fpvandoorn
Copy link
Member

Please fix error. If the change was simple, feel free to merge yourself

bors d+

@bors
Copy link

bors bot commented Jan 25, 2023

✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@github-actions github-actions bot added delegated and removed awaiting-review The author would like community review of the PR labels Jan 25, 2023
@YaelDillies
Copy link
Collaborator Author

Uhoh, looks like we're hitting the same problem as in #1238. I suspect it has to do with Function.Injective.addGroupWithOne now being reducible.

Posted on Zulip.

@eric-wieser
Copy link
Member

Looks like this is happy after merging master

@fpvandoorn
Copy link
Member

Ok, cool. Then let's merge this

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Feb 17, 2023
bors bot pushed a commit that referenced this pull request Feb 17, 2023
@YaelDillies @eric-wieser
feat: Missing transfer instances (#1725)
da75cad 
Match leanprover-community/mathlib#18247



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@bors
Copy link

bors bot commented Feb 17, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: Missing transfer instances [Merged by Bors] - feat: Missing transfer instances Feb 17, 2023
@bors bors bot closed this Feb 17, 2023
@bors bors bot deleted the injective_add_comm_monoid branch February 17, 2023 18:30
mo271 pushed a commit that referenced this pull request Feb 18, 2023
@YaelDillies @eric-wieser @mo271
feat: Missing transfer instances (#1725)
cd39681 
Match leanprover-community/mathlib#18247



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
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
delegated mathlib3-pair This PR is a forward-port of a mathlib3 PR or part of one, either under review or recently merged ready-to-merge This PR has been sent to bors.
Projects
No open projects
Forward ports of mathlib3
Status: Done
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@YaelDillies @fpvandoorn @eric-wieser