A collection of specific limit computations for IsROrC

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

@[deprecated IsROrC.tendsto_inverse_atTop_nhds_zero_nat]

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

Alias of IsROrC.tendsto_inverse_atTop_nhds_zero_nat.