mathlib

28b23c94 - feat(analysis/normed/group/seminorm): Group norms (#16237)

feat(analysis/normed/group/seminorm): Group norms (#16237) Define (additive) group norms, which are group seminorms `f` such that `f x = 0 → x = 0` (resp. `f x = 0 → x = 1`), along with their hom classes.