mathlib3

7c48d65c - feat(topology/algebra/group): define `has_continuous_inv` and `has_continuous_neg` type classes (#12748)

feat(topology/algebra/group): define `has_continuous_inv` and `has_continuous_neg` type classes (#12748) This creates the `has_continuous_inv` and `has_continuous_neg` type classes. The `has_continuous_neg` class will be helpful for generalizing `topological_ring` to the setting of `non_unital_non_assoc_semiring`s (see [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/continuous.20maps.20vanishing.20at.20infinity)). In addition, `ennreal` can have a `has_continuous_inv` instance.