mathlib

3a0b839b - feat(analysis/{normed/group}/seminorm): Hom classes for seminorms (#16227)

feat(analysis/{normed/group}/seminorm): Hom classes for seminorms (#16227) Introduce `add_group_seminorm_class`, `group_seminorm_class`, `seminorm_class`, the hom classes of `add_group_seminorm`, `group_seminorm`, `seminorm`.