Theorems · Theorem · real analysis

Polynomial.isEquivalent_atTop_div

∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P Q : Polynomial 𝕜)
  [OrderTopology 𝕜],
  Asymptotics.IsEquivalent Filter.atTop (fun x => Polynomial.eval x P / Polynomial.eval x Q) fun x =>
    P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree)

Defined in

Mathlib.Analysis.Polynomial.Basic

Cited by

5 results in Mathlib

Foundations

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

Assumes

NormedFieldLinearOrderIsStrictOrderedRingOrderTopology