Commit 2022-07-14 22:11 466b8922

feat(analysis/asymptotics/asymptotics): generalize, golf (#15010)

• add is_o_iff_nat_mul_le, is_o_iff_nat_mul_le', is_o_irrefl, is_O.not_is_o, is_o.not_is_O;
• generalize lemmas about 1 = o(f), 1 = O(f), f = o(1), f = O(1) to [has_one F] [norm_one_class F], add some @[simp] attrs;
• rename is_O_one_of_tendsto to filter.tendsto.is_O_one;
• golf some proofs