Zulip Chat Archive
Stream: condensed mathematics
Topic: SemiNormedGroup
Adam Topaz (May 19 2021 at 18:55):
Do we still need src/normed_group/SemiNormedGroup given docs#SemiNormedGroup ?
Johan Commelin (May 19 2021 at 19:17):
Hmm, no idea...
Johan Commelin (May 19 2021 at 19:17):
I guess we can get rid of most of it
Adam Topaz (May 19 2021 at 19:23):
I'm starting on 8.19 itself, and ran into this issue.
Adam Topaz (May 19 2021 at 19:23):
For now I'm using the SemiNormedGroup from LTE.
Adam Topaz (May 19 2021 at 19:24):
I'm also changing the statement of 8.19 a bit from what we discussed yesterday...
Last updated: Dec 20 2023 at 11:08 UTC