Commit 2026-01-26 11:17 216257fb

chore(Analysis/Asymptotics): remove unnecessary hypothesis from isEquivalent_of_tendsto_one (#34389) The condition ∀ᶠ x in l, v x = 0 → u x = 0 in isEquivalent_of_tendsto_one can be proven from the other assumption, Tendsto (u / v) l (𝓝 1). This PR proves that and removes the former condition.