feat(topology/algebra/normed_group): completion of normed groups (#6189) From lean-liquid
lean-liquid