mathlib3

73afba48 - refactor(analysis/normed/group/basic): Replace `normed_add_comm_group.core` with group norms (#16238)

refactor(analysis/normed/group/basic): Replace `normed_add_comm_group.core` with group norms (#16238) Delete `seminormed_add_comm_group.core`/`normed_add_comm_group.core` in favor of `add_group_norm`/`group_norm`. The former are unbundled prop versions of the latter, specialized to `∥ ∥`.