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.
Notification Bot (Jul 18 2020 at 10:07):
This topic was moved here from #new members > has_continuous_mul by Scott Morrison
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