mathlib3

17afc5c0 - feat(topology/algebra/group_with_zero): continuity lemma for division (#9959)

feat(topology/algebra/group_with_zero): continuity lemma for division (#9959) * This even applies when dividing by `0`. * From the sphere eversion project. * This PR mentions `filter.tendsto_prod_top_iff` which is added by #9958