Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-05 07:50 dc08f4d4

View on Github →

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

Estimated changes