mathlib3

99c23eaf - refactor(analysis/normed_space/basic): add semi_normed_group (#6888)

refactor(analysis/normed_space/basic): add semi_normed_group (#6888) This is part of a series of PR to have semi_normed_group (and related concepts) in mathlib. To keep the PR as small as possibile I just added the new class `semi_normed_group`. I didn't introduce anything like `semi_normed_ring` and I didn't do anything about morphisms.