Commit 2022-08-16 10:36 c553a824

feat(analysis/normed/group/basic): construct a normed group from a seminormed group satisfying ∥x∥ = 0 → x = 0 (#16066) This makes it more convenient to have a normed_add_comm_group instance as a special case of a general seminormed_add_comm_group without having to go back to the (pseudo) metric space level.