Theorem Tactic.ComputeAsymptotics.Monomial.toFun_tendsto_zero_of_firstNonzeroIsNeg

Modification history

2026-06-04 20:35
Mathlib/Tactic/ComputeAsymptotics/Multiseries/Monomial/Basic.lean
feat(Tactic/ComputeAsymptotics/Multiseries): compute limits of `Monomial`s (#37415) …
Added Tactic.ComputeAsymptotics.Monomial.toFun_tendsto_zero_of_firstNonzeroIsNegView on Github →