Commit 2022-09-30 18:24 73afba48
View on Github →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 ∥ ∥.