Mathlib v3 is deprecated. Go to Mathlib v4

Theorem uniform_space.completion.norm_coe

Modification history

2022-07-24 16:34
src/analysis/normed/group/completion.lean
chore(*): Rename `normed_group` to `normed_add_comm_group` (#15619) …
Modified uniform_space.completion.norm_coeView on Github →
2021-10-31 18:58
src/analysis/normed/group/completion.lean
chore(analysis): move more code out of `analysis.normed_space.basic` (#10055)
Modified uniform_space.completion.norm_coeView on Github →
2021-06-19 23:38
src/analysis/normed_space/basic.lean
refactor(topology/metric_space/isometry): move material about isometries of normed spaces (#8003) …
Modified uniform_space.completion.norm_coeView on Github →
2021-04-07 10:30
src/topology/algebra/normed_group.lean
refactor(topology/algebra/normed_group): generalize to semi_normed_group (#7066) …
Modified uniform_space.completion.norm_coeView on Github →
2021-02-16 18:36
src/topology/algebra/normed_group.lean
feat(topology/algebra/normed_group): completion of normed groups (#6189) …
Added uniform_space.completion.norm_coeView on Github →