A collection of specific limit computations for RCLike

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

@[deprecated RCLike.tendsto_inverse_atTop_nhds_zero_nat]

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

Alias of RCLike.tendsto_inverse_atTop_nhds_zero_nat.

theorem RCLike.tendsto_add_mul_div_add_mul_atTop_nhds {𝕜 : Type u_1} [RCLike 𝕜] (a : 𝕜) (b : 𝕜) (c : 𝕜) {d : 𝕜} (hd : d ≠ 0) : Filter.Tendsto (fun (k : ℕ) => (a + c * ↑k) / (b + d * ↑k)) Filter.atTop (nhds (c / d))