## Stream: maths

### Topic: has_continuous_mul

#### 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