Skip to content

[Merged by Bors] - fix(Algebra/Order/CauSeq/Completion): fix qsmul instance diamond#11263

Closed
eric-wieser wants to merge 9 commits intomasterfrom
eric-wieser/CauSeq.Completion-qsmul
Closed

[Merged by Bors] - fix(Algebra/Order/CauSeq/Completion): fix qsmul instance diamond#11263
eric-wieser wants to merge 9 commits intomasterfrom
eric-wieser/CauSeq.Completion-qsmul

Conversation

@eric-wieser
Copy link
Copy Markdown
Member

@eric-wieser eric-wieser commented Mar 9, 2024

@eric-wieser eric-wieser added awaiting-review blocked-by-core-PR This PR depends on a PR to Core/Std awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Mar 9, 2024
@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 9, 2024
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Mar 9, 2024
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 9, 2024
@ghost
Copy link
Copy Markdown

ghost commented Mar 9, 2024

This PR/issue depends on:

@eric-wieser eric-wieser removed the blocked-by-core-PR This PR depends on a PR to Core/Std label Mar 10, 2024
@mattrobball
Copy link
Copy Markdown
Contributor

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Mar 10, 2024
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 10, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title fix(Algebra/Order/CauSeq/Completion): fix qsmul instance diamond [Merged by Bors] - fix(Algebra/Order/CauSeq/Completion): fix qsmul instance diamond Mar 10, 2024
@mathlib-bors mathlib-bors bot closed this Mar 10, 2024
@mathlib-bors mathlib-bors bot deleted the eric-wieser/CauSeq.Completion-qsmul branch March 10, 2024 15:45
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

ready-to-merge This PR has been sent to bors.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants