Mathlib v3 is deprecated. Go to Mathlib v4

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_semirings (see Zulip thread). In addition, ennreal can have a has_continuous_inv instance.

Estimated changes