Theorem Asymptotics.isEquivalent_of_tendsto_one

Modification history

2026-01-26 11:17
Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean
chore(Analysis/Asymptotics): remove unnecessary hypothesis from `isEquivalent_of_tendsto_one` (#34389) …
Modified Asymptotics.isEquivalent_of_tendsto_oneView on Github →
2023-04-17 06:46
Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean
feat: port Analysis.Asymptotics.AsymptoticEquivalent (#3417)
Added Asymptotics.isEquivalent_of_tendsto_oneView on Github →