basic): closure of `{0}` in a seminormed group (#17287)

Commit

3 years ago

feat(analysis/normed/group/basic): closure of `{0}` in a seminormed group (#17287)

Author

ADedecker

Parents