Generalise Asymptotics API to drop commutative assumptions

[grhkm21]

Extracted from #16015. A lot of lemmas in Analysis/Asymptotics/Asymptotics.lean have unnecessary commutative requirements. For example, by applying the follow change on line 59:

- variable [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G']
+ variable [SeminormedAddGroup E'] [SeminormedAddGroup F'] [SeminormedAddGroup G']

One only gets 50 errors in the file, with the first error occurring on line 623, despite there being more theorems using those variables:

rg "^theorem.+[EFGfgk]'[^']" Mathlib/Analysis/Asymptotics/Asymptotics.lean | wc -l
104

Relevant files that may also require fixing include Mathlib/Analysis/Normed/Field/Basic.lean (e.g. theorem norm_norm doesn't require commutativity), as they are used in the Asymptotics file.