mathlib

fb1848bb - refactor(topology/algebra/open_subgroup) Finish TODO (#1202)

refactor(topology/algebra/open_subgroup) Finish TODO (#1202) * Create .DS_Store * Revert "Create .DS_Store" This reverts commit 5612886d493aef59205eddc5a34a75e6e5ba22c1. * Finish TODO * Update src/topology/algebra/open_subgroup.lean Co-Authored-By: Johan Commelin <johan@commelin.net>