feat(analysis/seminorm): add add_group_seminorm (#14336)
We introduce `add_group_seminorm` and refactor `seminorm` to extend this new definition. This new `add_group_seminorm` structure will also be used in #14115 to define `ring_seminorm`.
Co-authored-by: María Inés de Frutos-Fernández <88536493+mariainesdff@users.noreply.github.com>
Co-authored-by: Oliver Nash <github@olivernash.org>
