order): ⁻¹ continuous for linear ordered fields (#15022)

Commit

3 years ago

feat(topology/algebra/order): ⁻¹ continuous for linear ordered fields (#15022) Closes #12781. Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>

Author

ericrbg

Parents

44999a92

mathlib be53c7cb - feat(topology/algebra/order): ⁻¹ continuous for linear ordered fields (#15022)

mathlib
be53c7cb - feat(topology/algebra/order): ⁻¹ continuous for linear ordered fields (#15022)