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.

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

[Merged by Bors] - split(analysis/convex/slope): split slope results off analysis.convex.function #9444

Closed
wants to merge 1 commit into from

Conversation

YaelDillies
Copy link
Collaborator


The file is about to get big again because of strictly convex/strictly concave functions.

I credited Yury for #1819 and Malo for #4307

Open in Gitpod

@YaelDillies YaelDillies added the awaiting-review The author would like community review of the PR label Sep 29, 2021
@YaelDillies YaelDillies changed the title split(analysis/convex/slope): split slope resultsinequalities off analysis.convex.function split(analysis/convex/slope): split slope results off analysis.convex.function Sep 29, 2021
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors d+

@bors
Copy link

bors bot commented Sep 29, 2021

✌️ 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.

@jcommelin jcommelin added awaiting-CI The author would like to see what CI has to say before doing more work. ready-for-bors and removed awaiting-review The author would like community review of the PR labels Sep 29, 2021
@github-actions github-actions bot added the delegated The PR author may merge after reviewing final suggestions. label Sep 29, 2021
@YaelDillies
Copy link
Collaborator Author

bors merge

bors bot pushed a commit that referenced this pull request Sep 29, 2021
@bors
Copy link

bors bot commented Sep 29, 2021

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Sep 29, 2021
@bors
Copy link

bors bot commented Sep 29, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title split(analysis/convex/slope): split slope results off analysis.convex.function [Merged by Bors] - split(analysis/convex/slope): split slope results off analysis.convex.function Sep 29, 2021
@bors bors bot closed this Sep 29, 2021
@YaelDillies YaelDillies deleted the split_slope branch September 30, 2021 07:41
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
awaiting-CI The author would like to see what CI has to say before doing more work. delegated The PR author may merge after reviewing final suggestions. ready-for-bors
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants