mathlib3

d75da1a2 - feat(topology/algebra/group_with_zero): introduce `has_continuous_inv'` (#4804)

feat(topology/algebra/group_with_zero): introduce `has_continuous_inv'` (#4804) Move lemmas about continuity of division from `normed_field`, add a few new lemmas, and introduce a new typeclass. Also use it for `nnreal`s.