∀ {𝕜 : Type u_4} [inst : DivisionSemiring 𝕜] [inst_1 : CharZero 𝕜] [inst_2 : TopologicalSpace 𝕜] [ContinuousSMul ℚ≥0 𝕜]
  [ContinuousMul 𝕜] (C : 𝕜), Filter.Tendsto (fun n => C / ↑n) Filter.atTop (nhds 0)