Theorem Asymptotics.IsBigOTVS.of_egauge_le_mul

Modification history

2026-01-27 17:10
Mathlib/Analysis/Asymptotics/TVS.lean
feat(Asymptotics/TVS): prove that `IsBigOTVS` is equivalent to `IsBigO` (#34074)
Added Asymptotics.IsBigOTVS.of_egauge_le_mulView on Github →