mathlib

f5afe205 - split(analysis/normed/group/seminorm): Split off `analysis.seminorm` (#16152)

split(analysis/normed/group/seminorm): Split off `analysis.seminorm` (#16152) Move `group_seminorm` and `add_group_seminorm` to a new file `analysis.normed.group.seminorm`. Move `norm_add_group_seminorm` to `analysis.normed.group.basic`. Remove the `nonneg` field from `add_group_seminorm` and `group_seminorm` because it is redundant.