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

[Merged by Bors] - chore(topology/continuous_function/zero_at_infty): add is_central_scalar instance#13710

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

[Merged by Bors] - chore(topology/continuous_function/zero_at_infty): add is_central_scalar instance#13710
eric-wieser wants to merge 1 commit intomasterfrom
eric-wieser/zero_at_infty_continuous_map.is_central_scalar

Conversation

@eric-wieser
Copy link
Copy Markdown
Member


Open in Gitpod

@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 labels Apr 26, 2022
eric-wieser added a commit that referenced this pull request Apr 26, 2022
@dupuisf
Copy link
Copy Markdown
Collaborator

dupuisf commented Apr 26, 2022

bors r+

@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 26, 2022
bors bot pushed a commit that referenced this pull request Apr 26, 2022
@bors
Copy link
Copy Markdown

bors bot commented Apr 26, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore(topology/continuous_function/zero_at_infty): add is_central_scalar instance [Merged by Bors] - chore(topology/continuous_function/zero_at_infty): add is_central_scalar instance Apr 26, 2022
@bors bors bot closed this Apr 26, 2022
@bors bors bot deleted the eric-wieser/zero_at_infty_continuous_map.is_central_scalar branch April 26, 2022 20:18
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