mathlib3

dc08f4d4 - feat(analysis): define asymptotic equivalence of two functions (#4979)

feat(analysis): define asymptotic equivalence of two functions (#4979) This defines the relation `is_equivalent u v l`, which means that `u-v` is little o of `v` along the filter `l`. It is required to state, for example, Stirling's formula, or the prime number theorem