∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P : Polynomial 𝕜)
  [OrderTopology 𝕜], Filter.Tendsto (fun x => |Polynomial.eval x P|) Filter.atTop Filter.atTop ↔ 0 < P.degree