has_continuous_mul

Stream: new members

[Nicolò Cavalleri]

I need to generalize topological_monoid to topological_semigroup. At this point I do not see why not defining

class has_continuous_mul (α : Type*) [topological_space α] [has_mul α] : Prop :=
(continuous_mul : continuous (λp:α×α, p.1 * p.2))

so, first question: does it still make sense to have topological monoid at this point? It can be obtained just by combining monoid and has_continuous_mul. I would just delete it. Second question: in case it is a good idea to keep topological_monoidjust for psychological reasons, I do not know how to keep it. If I define

abbreviation topological_monoid (α : Type*) [topological_space α] [monoid α]
:= topological_semigroup α

then any structure, like semiring, extending topological_monoid breaks. Should I then make structures inherit from has_continuous_mul and manually define coercions to topological_monoid? I mean at this point it looks more logic to delete it and just use has_continuous_mul. If I define it like

class topological_monoid (α : Type*) [topological_space α] [monoid α]
extends topological_semigroup α: Prop

then, because of protected inheritance, all the files that try to define a topological_monoid with one constructor break. Is there any way to get rid of protected inheritance for this class and make it so that it can be constructed with one constructor? This is the only way I see to try to keep it.