Zulip Chat Archive

Stream: maths

Topic: has_continuous_mul

view this post on Zulip Patrick Massot (Jul 18 2020 at 10:06):

I think you can get rid of topological_monoid. And I'm sure you should get rid of the habit of posting in "new members". This question has nothing to do here.

view this post on Zulip Notification Bot (Jul 18 2020 at 10:07):

This topic was moved here from #new members > has_continuous_mul by Scott Morrison

view this post on Zulip Yury G. Kudryashov (Jul 18 2020 at 15:46):

It might make sense to add has_continuous_inv as well, and make topological_group extend these two classes. Then we'll have has_continuous_inv ennreal. And has_continuous_inv' could be a type class for "inv is continuous at every nonzero element"

Last updated: May 09 2021 at 11:09 UTC