Mathlib Changelog
v4
Changelog
About
Github
Theorem
Asymptotics.IsLittleO.of_tendsto_div_atBot
Modification history
2026-02-11 11:43
Mathlib/Analysis/Asymptotics/Lemmas.lean
feat(Tactic/ComputeAsymptotics): lemmas for converting different goals to `Tendsto f atTop l` (#34403) …
Added
Asymptotics.IsLittleO.of_tendsto_div_atBot
View on Github →