Subgroup of topological group

Stream: Is there code for X?

[Anatole Dedecker]

Am I blind or do we not have

instance [topological_space α] [group α] [topological_group α] (S : subgroup α) :
topological_group S := sorry

[Kevin Buzzard]

lol Maria Ines asked me the same question today but for topological rings :-) You might be right! (I told her that she was one of the Lean experts in topological rings so not to ask me :-) )

[Anatole Dedecker]

#10491