Commit 2022-04-29 11:14 889e9564

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.