Commit 2022-03-24 12:01 7c48d65c
View on Github →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). In addition, ennreal
can have a has_continuous_inv
instance.