Theorems · Theorem · real analysis

Polynomial.isEquivalent_atBot_lead

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

Defined in

Mathlib.Analysis.Polynomial.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedFieldLinearOrderIsStrictOrderedRingOrderTopology