mathlib3

9e9cc57d - feat(analysis/asymptotics/asymptotics): add `is_O_const_iff` (#14472)

feat(analysis/asymptotics/asymptotics): add `is_O_const_iff` (#14472) * use `f =ᶠ[l] 0` instead of `∀ᶠ x in l, f x = 0` in `is_{O_with,O,o}_zero_right_iff`; * generalize these lemmas from `0` in a `normed_group` to `0` in a `semi_normed_group`; * add `is_O.is_bounded_under_le`, `is_O_const_of_ne`, and `is_O_const_iff`.