Theorem Asymptotics.IsEquivalent.trans_isBigO

Modification history

2023-07-02 04:04

Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean

feat(Analysis/Asymptotics/AsymptoticEquivalent): add `Trans` instances for `IsEquivalent` (#5572) …

Added Asymptotics.IsEquivalent.trans_isBigO View on Github →