Commit 2021-04-07 10:30 9157b577

View on Github →

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).

Estimated changes

Modified src/topology/algebra/normed_group.lean

modified theorem uniform_space.completion.norm_coe

Modified src/topology/metric_space/completion.lean