mathlib

7ce2bb4a - feat(order/filter/at_top_bot): add lemmas about convergence of `λ x, r * f x` to `±∞` (#16355)

feat(order/filter/at_top_bot): add lemmas about convergence of `λ x, r * f x` to `±∞` (#16355) Other API changes: * assume `m ≠ 0` instead of `1 ≤ m` in `le_self_pow`; * generalize `linear_ordered_semiring.to_no_max_order` to `ordered_semiring.to_no_max_order`.