mathlib3

b87c2677 - feat(topology/algebra/group): add small topology lemma (#12931)

feat(topology/algebra/group): add small topology lemma (#12931) Adds a small topology lemma by splitting `compact_open_separated_mul` into `compact_open_separated_mul_left/right`, which was useful in my proof of `Steinhaus theorem` (see #12932), as in a non-abelian group, the current version was not sufficient. Co-authored-by: YaelDillies <yael.dillies@gmail.com>