Commit 2022-03-29 11:26 b87c2677

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.