mathlib3

d43f202f - feat(analysis/analytic/basic): `f (x + y) - p.partial_sum n y = O(∥y∥ⁿ)` (#5756)

feat(analysis/analytic/basic): `f (x + y) - p.partial_sum n y = O(∥y∥ⁿ)` (#5756) ### Lemmas about analytic functions * add `has_fpower_series_on_ball.uniform_geometric_approx'`, a more precise version of `has_fpower_series_on_ball.uniform_geometric_approx`; * add `has_fpower_series_at.is_O_sub_partial_sum_pow`, a version of the Taylor formula for an analytic function; ### Lemmas about `homeomorph` and topological groups * add `simp` lemmas `homeomorph.coe_mul_left` and `homeomorph.mul_left_symm`; * add `map_mul_left_nhds` and `map_mul_left_nhds_one`; * add `homeomorph.to_equiv_injective` and `homeomorph.ext`; ### Lemmas about `is_O`/`is_o` * add `simp` lemmas `asymptotics.is_O_with_map`, `asymptotics.is_O_map`, and `asymptotics.is_o_map`; * add `asymptotics.is_o_norm_pow_norm_pow` and `asymptotics.is_o_norm_pow_id`; ### Misc changes * rename `div_le_iff_of_nonneg_of_le` to `div_le_of_nonneg_of_le_mul`; * add `continuous_linear_map.op_norm_le_of_nhds_zero`; * golf some proofs.