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






leanprover-community/mathlib,leanprover-community/mathlib