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 →