mathlib3

724f804b - refactor(src/analysis/normed_space/linear_isometry): generalize to semi_normed_group (#7122)

refactor(src/analysis/normed_space/linear_isometry): generalize to semi_normed_group (#7122) This is part of a series of PR to include the theory of seminormed things in mathlib. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>