feat(analysis/normed_space/SemiNormedGroup): has_cokernels (#7628)

Cokernels in SemiNormedGroup₁ and SemiNormedGroup

We show that SemiNormedGroup₁ has cokernels (for which of course the cokernel.π f maps are norm non-increasing), as well as the easier result that SemiNormedGroup has cokernels. So far, I don't see a way to state nicely what we really want: SemiNormedGroup has cokernels, and cokernel.π f is norm non-increasing. The problem is that the limits API doesn't promise you any particular model of the cokernel, and in SemiNormedGroup one can always take a cokernel and rescale its norm (and hence making cokernel.π f arbitrarily large in norm), obtaining another categorical cokernel.