mathlib3

c553a824 - feat(analysis/normed/group/basic): construct a normed group from a seminormed group satisfying `∥x∥ = 0 → x = 0` (#16066)

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.