-
Notifications
You must be signed in to change notification settings - Fork 297
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
feat(analysis/specific_limits/complex) #18887
Conversation
Specific limits complex numbers Prerequisite for upcoming Hadamard Three Lines Theorem. Separate from basic to avoid adding dependencies. Proof of lemma by Patrick Massot
I'm surprised we can't state this more generally; is it true for any ℝ-algebra? |
Added a lemma for the limit of `1/n` into an `ℝ` algebra.
Simplified proofs in term of ℝ algebras
Why do you remove the TODO comment on the following lemma? I don't think this lemma solves that problem -- the point of the comment is that it would be nice to cover topological rings which aren't algebras over the reals. |
Re-added the TODO
My mistake! |
I've created a zulip thread about this PR. |
I left a comment in the Zulip thread with a |
This PR introduces a single new lemma about the limit of 1 / n as n → ∞ in the complex numbers. It has been placed in a new file for two reasons: the obvious file to put it (analysis/specific_limits/basic) does not have the required imports, and it also makes porting easier since basic has already been ported to mathlib4.
Note that this is a prerequisite for an upcoming PR for the Hadamard three-line theorem.
Finally, thanks to Patrick Massot for supplying the actual proof on Zulip a while back!