Yaël Dillies

Here is [the thread](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Misc.20semigroup.20stuff).

I made Kyle's characterisation the definition, renamed the predicate to something more human-readable. I also generalized the predicate, but are you sure this is what you want, @collares? My `delete_far`...

Currently, we have two ways to talk about (additive group) seminorms: * `add_group_seminorm` * `seminormed_add_comm_group.core` I want to get rid of the second way and make seminormed groups depend on...

bors merge

If you agree with the folder scheme I described at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Reorganising.20norms, could you move the new material to `analysis.normed.field.seminorm` or `analysis.normed.ring.seminorm`? I suspect this second option only makes sense if...

Well I would prefer for you to introduce the hom classes straight away. If you don't know how to, I can do it.

Here they are.

I think it's fair merging now

The changes to the proof are just adding `casesI nonempty_fintype _`, as preconized by the `fintype_finite` linter.

This is all just `fintype_finite`: * The "anti-golf" is required because the previous proof was creating another metavariable midway that appeared in a `fintype` instance. Now that I need to...