mathlib
05ef6940 - refactor(topology/instances/ennreal): make `ennreal` an instance of `has_continuous_inv` (#12806)

Commit
3 years ago
refactor(topology/instances/ennreal): make `ennreal` an instance of `has_continuous_inv` (#12806) Prior to the type class `has_continuous_inv`, `ennreal` had to have it's own hand-rolled `ennreal.continuous_inv` statement. This replaces it with a `has_continuous_inv` instance. - [x] depends on: #12748
Author
Parents
Loading