mathlib3

889e9564 - chore(analysis/asymptotics/asymptotics): relax `normed_group` to `semi_normed_group` in lemmas (#13642)

chore(analysis/asymptotics/asymptotics): relax `normed_group` to `semi_normed_group` in lemmas (#13642) This file already uses `E` vs `E'` for `has_norm` vs `normed_group`. This adds an `E''` to this naming scheme for `normed_group`, and repurposes `E'` to `semi_normed_group`. The majority of the lemmas in this file generalize without any additional work. I've not attempted to relax the assumptions on lemmas where any proofs would have to change. Most of them would need their assumptions changing from `c ≠ 0` to `∥c∥ ≠ 0`, which is likely to be annoying. In one place this results in dot notation breaking as the typeclass can no longer be found by unification.