mathlib

0d7ddf1f - chore(order/filter/at_top_bot): add/rename lemmas about limits like `±∞*c` (#5333)

chore(order/filter/at_top_bot): add/rename lemmas about limits like `±∞*c` (#5333) ### New lemmas * `filter.tendsto.nsmul_at_top` and `filter.tendsto.nsmul_at_bot`; * `filter.tendsto_mul_self_at_top`; * `filter.tendsto.at_top_mul_at_bot`, `filter.tendsto.at_bot_mul_at_top`, `filter.tendsto.at_bot_mul_at_bot`; * `filter.tendsto.at_top_of_const_mul`, `filter.tendsto.at_top_of_mul_const`; * `filter.tendsto.at_top_div_const`, `filter.tendsto.neg_const_mul_at_top`, `filter.tendsto.at_top_mul_neg_const`, `filter.tendsto.const_mul_at_bot`, `filter.tendsto.at_bot_mul_const`, `filer.tendsto.at_bot_div_const`, `filter.tendsto.neg_const_mul_at_bot`, `filter.tendsto.at_bot_mul_neg_const`. ### Renamed lemmas * `tendsto_pow_at_top` → `filter.tendsto_pow_at_top`; * `tendsto_at_top_mul_left` → `filter.tendsto.const_mul_at_top'`; * `tendsto_at_top_mul_right` → `filter.tendsto.at_top_mul_const'`; * `tendsto_at_top_mul_left'` → `filter.tendsto.const_mul_at_top`; * `tendsto_at_top_mul_right'` → `filer.tendsto.at_top_mul_const`; * `tendsto_mul_at_top` → `filter.tendsto.at_top_mul`; * `tendsto_mul_at_bot` → `filter.tendsto.at_top_mul_neg`; * `tendsto_at_top_mul_at_top` → `filter.tendsto.at_top_mul_at_top`.