Eric Wieser
Eric Wieser
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
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. Is it the case that anything satisfying...
> If you have an `is_seminorm_ring` on `k` that satisfies the triangle inequality (which I probably should include in the definition) This was really what I was getting at; it...
Ah, I understand your comment now; I hadn't realized that `seminorm 𝕜 E` relied on an underlying global norm on `𝕜`
(misclick, sorry)
> Ah, I understand your comment now; I hadn't realized that `seminorm 𝕜 E` relied on an underlying global norm on `𝕜` Thinking again, I don't think this matters; you...
~~I think `add_group_seminorm.trivial_norm f` is just `f ≠ 0`?~~
> but I can do without if it seems too specialized. I would lean towards saying it does; Let's wait till the other PRs #15541 are blocked by are resolved...
Do we really want to do this? I feel like mathematically `is_scalar_tower` carries much more meaning than `smul_assoc_class`. The Zulip thread you link to doesn't discuss this rename; can you...