normed_group): completion of normed groups (#6189)

Commit

4 years ago

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

Author

jcommelin

Parents