has_continuous_mul

Stream: maths

[Patrick Massot]

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]

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

[Yury G. Kudryashov]

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"