mathlib

9157b577 - refactor(topology/algebra/normed_group): generalize to semi_normed_group (#7066)

refactor(topology/algebra/normed_group): generalize to semi_normed_group (#7066) The completion of a `semi_normed_group` is a `normed_group` (and similarly for `pseudo_metric_space`).