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

[Merged by Bors] - chore(linear_algebra/alternating): add an is_central_scalar instance#15359

Closed
eric-wieser wants to merge 1 commit intomasterfrom
eric-wieser/alternating_map.is_central_scalar
Closed

[Merged by Bors] - chore(linear_algebra/alternating): add an is_central_scalar instance#15359
eric-wieser wants to merge 1 commit intomasterfrom
eric-wieser/alternating_map.is_central_scalar

Conversation

@eric-wieser
Copy link
Copy Markdown
Member

@eric-wieser eric-wieser commented Jul 14, 2022


Open in Gitpod

Split from #10716

@eric-wieser eric-wieser added easy < 20s of review time. See the lifecycle page for guidelines. 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. labels Jul 14, 2022
eric-wieser added a commit that referenced this pull request Jul 14, 2022
@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 Jul 14, 2022
@robertylewis
Copy link
Copy Markdown
Member

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 Jul 15, 2022
@bors
Copy link
Copy Markdown

bors bot commented Jul 15, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore(linear_algebra/alternating): add an is_central_scalar instance [Merged by Bors] - chore(linear_algebra/alternating): add an is_central_scalar instance Jul 15, 2022
@bors bors bot closed this Jul 15, 2022
@bors bors bot deleted the eric-wieser/alternating_map.is_central_scalar branch July 15, 2022 15:49
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Labels

easy < 20s of review time. See the lifecycle page for guidelines. ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants