Mathlib v3 is deprecated. Go to Mathlib v4

Theorem asymptotics.is_O_with.const_mul_right'

Modification history

2022-01-05 23:45
src/analysis/asymptotics/asymptotics.lean
chore(*): notation for `units` (#11236)
Modified asymptotics.is_O_with.const_mul_right'View on Github →
2020-01-08 13:16
src/analysis/asymptotics.lean
refactor(analysis/asymptotics): introduce `is_O_with` (#1857) …
Added asymptotics.is_O_with.const_mul_right'View on Github →