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

[Merged by Bors] - feat(analysis/analytic/inverse): convergence of the inverse of a power series #5854

Closed
wants to merge 22 commits into from
Closed

[Merged by Bors] - feat(analysis/analytic/inverse): convergence of the inverse of a power series #5854

wants to merge 22 commits into from

Conversation

sgouezel
Copy link
Collaborator

@sgouezel sgouezel commented Jan 22, 2021 •
edited by github-actions bot
Loading

@github-actions github-actions bot added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Jan 22, 2021
@sgouezel sgouezel mentioned this pull request Jan 22, 2021
Closed
1 task
@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Jan 23, 2021
@github-actions github-actions bot added merge-conflict Please `git merge origin/master` then a bot will remove this label. and removed merge-conflict Please `git merge origin/master` then a bot will remove this label. blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. labels Jan 27, 2021
@github-actions
Copy link

🎉 Great news! Looks like all the dependencies have been resolved:

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Jan 31, 2021
@sgouezel sgouezel added the awaiting-review The author would like community review of the PR label Jan 31, 2021
@sgouezel sgouezel changed the title feat(analysis/anaytic/inverse): convergence of the inverse of a power series feat(analysis/analytic/inverse): convergence of the inverse of a power series Jan 31, 2021
jcommelin
jcommelin approved these changes Feb 10, 2021
View reviewed changes
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.

This is extremely well-written and well documented. With a pretty smart trick to get a relatively painfree proof.

Thanks 🎉

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 Feb 10, 2021
bors bot pushed a commit that referenced this pull request Feb 11, 2021
@sgouezel
feat(analysis/analytic/inverse): convergence of the inverse of a powe…
c70feeb 
…r series (#5854)

If a formal multilinear series has a positive radius of convergence, then its inverse also does.
@bors
Copy link

bors bot commented Feb 11, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(analysis/analytic/inverse): convergence of the inverse of a power series [Merged by Bors] - feat(analysis/analytic/inverse): convergence of the inverse of a power series Feb 11, 2021
@bors bors bot closed this Feb 11, 2021
@bors bors bot deleted the analytic_inverse branch February 11, 2021 04:10
jcommelin pushed a commit that referenced this pull request Feb 11, 2021
@sgouezel @jcommelin
feat(analysis/analytic/inverse): convergence of the inverse of a powe…
ceef000 
…r series (#5854)

If a formal multilinear series has a positive radius of convergence, then its inverse also does.
b-mehta pushed a commit that referenced this pull request Apr 2, 2021
@sgouezel @b-mehta
feat(analysis/analytic/inverse): convergence of the inverse of a powe…
37f0efc 
…r series (#5854)

If a formal multilinear series has a positive radius of convergence, then its inverse also does.
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@jcommelin jcommelin jcommelin approved these changes

@hrmacbeth hrmacbeth Awaiting requested review from hrmacbeth

Assignees
No one assigned
Labels
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
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@sgouezel @jcommelin