feat(topology/algebra/group): continuous div lemmas (#9905)
* From the sphere eversion project
* There were already some lemmas about `sub`, now they also have multiplicative versions
* Add more lemmas about `div` being continuous
* Add `continuous_at.inv`
* Rename `nhds_translation` -> `nhds_translation_sub`.
