María Inés de Frutos-Fernández
María Inés de Frutos-Fernández
> Are you aware of the `seminorm` structure we already have? I'm a little worried this is duplicating it, just with a different sort of bundling The structure [seminorm](https://leanprover-community.github.io/mathlib_docs/analysis/seminorm.html#seminorm) is...
> I think if we really want both `is_seminorm` and `seminorm`, then we should rename the concept in this file to `is_mul_seminorm` or similar. I would not mind renaming `is_seminorm`...
> This was really what I was getting at; it seems odd for a seminorm not to satisfy the triangle inequality. Yes, this was an oversight on my part (since...
> Thinking again, I don't think this matters; you can always just set `𝕜 = punit` and then it becomes irrelevant. So maybe extending `seminorm` is still the right way...
> 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've moved it to `analysis.normed.ring.seminorm` (to me that...
~~@YaelDillies, you said that #16237 already added `add_group_seminorm.trivial_norm` but I can't find it. Does it have a different name?~~ I guess it's the 1 norm.
Can I go ahead and merge it now?
> Well I would prefer for you to introduce the hom classes straight away. If you don't know how to, I can do it. I am happy to do that...