Skip to content

[Merged by Bors] - chore: Missing to_additive on CommSemigroup.isCentralScalar#2344

Closed
YaelDillies wants to merge 8 commits intomasterfrom
upper_lower_topology
Closed

[Merged by Bors] - chore: Missing to_additive on CommSemigroup.isCentralScalar#2344
YaelDillies wants to merge 8 commits intomasterfrom
upper_lower_topology

Conversation

@YaelDillies
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies commented Feb 17, 2023 •
edited by eric-wieser
Loading

The SHA was already updated in #2498, but the #align was forgotten, and the instance name was incorrectly generated.

Match leanprover-community/mathlib3#16975.

Open in Gitpod

@YaelDillies YaelDillies added awaiting-review mathlib3-pair This PR is a forward-port of a mathlib3 PR or part of one, either under review or recently merged labels Feb 17, 2023
eric-wieser
eric-wieser approved these changes Feb 17, 2023
View reviewed changes
Copy link
Copy Markdown
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

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

bors merge

Thanks!

@kim-em kim-em added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Feb 17, 2023
bors bot pushed a commit that referenced this pull request Feb 17, 2023
@YaelDillies
chore: Missing to_additive on CommSemigroup.isCentralScalar (#2344)
1391918 
Match leanprover-community/mathlib3#16975
@bors
Copy link
Copy Markdown

bors bot commented Feb 17, 2023

Build failed:

@eric-wieser eric-wieser added awaiting-author A reviewer has asked the author a question or requested changes. and removed ready-to-merge This PR has been sent to bors. labels Feb 17, 2023
@eric-wieser
Copy link
Copy Markdown
Member

eric-wieser commented Feb 17, 2023

bors d+

Did we misport something elsewhere? Or forget to forward-port something?

@bors
Copy link
Copy Markdown

bors bot commented Feb 17, 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 the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Feb 17, 2023
@YaelDillies
Copy link
Copy Markdown
Contributor Author

YaelDillies commented Feb 17, 2023

Nothing misported, but to_additive is missing the translation IsCentralScalar → IsCentralVAdd. @fpvandoorn, can you explain how to do the translation? I tried something but it didn't work.

eric-wieser
eric-wieser reviewed Feb 17, 2023
View reviewed changes
@mo271 mo271 mentioned this pull request Feb 26, 2023
Closed
1 task
@eric-wieser eric-wieser mentioned this pull request Feb 27, 2023
Closed
@fpvandoorn
Copy link
Copy Markdown
Member

fpvandoorn commented Mar 1, 2023

Thanks!

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Mar 1, 2023
bors bot pushed a commit that referenced this pull request Mar 1, 2023
@YaelDillies @eric-wieser @fpvandoorn
chore: Missing to_additive on CommSemigroup.isCentralScalar (#2344)
90bb14f 
The SHA was already updated in #2498, but the `#align` was forgotten, and the instance name was incorrectly generated.

Match leanprover-community/mathlib3#16975.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Mar 1, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore: Missing to_additive on CommSemigroup.isCentralScalar [Merged by Bors] - chore: Missing to_additive on CommSemigroup.isCentralScalar Mar 1, 2023
@bors bors bot closed this Mar 1, 2023
@bors bors bot deleted the upper_lower_topology branch March 1, 2023 18:09
bors bot pushed a commit that referenced this pull request Mar 2, 2023
@mo271
feat: port Topology.Algebra.Order.UpperLower (#2503)
4f884ff 
- [x] depends on: #2344



Co-authored-by: Moritz Firsching <firsching@google.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@eric-wieser eric-wieser eric-wieser approved these changes

@fpvandoorn fpvandoorn fpvandoorn left review comments

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). 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: SHA added

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@YaelDillies @eric-wieser @fpvandoorn @kim-em