Commit 2023-08-08 00:12 d71f10bb
View on Github →feat(analysis/specific_limits): Lemma for limit of 1 / n as n → ∞ in real algebras (#6249) 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 to avoid import creep: the obvious file in which to put it (Analysis.SpecificLimits.Basic) does not have the required imports.
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!