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] - refactor(analysis/analytic/basic): redefine formal_multilinear_series.radius
#5349
Conversation
…series` to a new file
…s.radius` With the new definition, (a) some proofs get much shorter; (b) we don't need `rpow` in `analytic/basic`.
Thanks, this is something that had to be done to redefine the exponential using power series while avoiding loops. Still, could you prove that the new definition equals the liminf definition of the convergence radius, in another file, as this definition can be handy sometimes? |
🎉 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! |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nice!
bors d+
✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
…s.radius` (#5349) With the new definition, (a) some proofs get much shorter; (b) we don't need `rpow` in `analytic/basic`.
Pull request successfully merged into master. Build succeeded! And happy new year! 🎉 |
formal_multilinear_series.radius
formal_multilinear_series.radius
With the new definition, (a) some proofs get much shorter; (b) we
don't need
rpow
inanalytic/basic
.formal_multilinear_series
to a new file #5348nnnorm
#5532tsum_mul_left/right
#5533