A collection of specific limit computations for IsROrC

theorem IsROrC.tendsto_inverse_atTop_nhds_0_nat (𝕜 : Type u_1) [IsROrC 𝕜] : Filter.Tendsto (fun n => (↑n)⁻¹) Filter.atTop (nhds 0)