mathlib

d1bd9c5d - chore(*): Rename `normed_group` to `normed_add_comm_group` (#15619)

chore(*): Rename `normed_group` to `normed_add_comm_group` (#15619) * `normed_group` → `normed_add_comm_group` * `semi_normed_group` → `seminormed_add_comm_group`. Elision of the underscore corresponds to `seminorm` (and to counterbalance the name being sensibly longer). * `normed_group_hom` → `normed_add_group_hom`