Theorems · Theorem · real analysis

Polynomial.div_tendsto_atBot_leadingCoeff_div_of_degree_eq

∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P Q : Polynomial 𝕜)
  [OrderTopology 𝕜],
  P.degree = Q.degree →
    Filter.Tendsto (fun x => Polynomial.eval x P / Polynomial.eval x Q) Filter.atBot
      (nhds (P.leadingCoeff / Q.leadingCoeff))

Defined in

Mathlib.Analysis.Polynomial.Basic

Cited by

0 results in Mathlib

Foundations

Depth 172 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedFieldLinearOrderIsStrictOrderedRingOrderTopology