Topic: Missing instance
Yury G. Kudryashov (Apr 06 2020 at 18:44):
Am I right that we have no
linear_ordered_field → linear_ordered_comm_ring instance?
Patrick Massot (Apr 06 2020 at 19:08):
The instances listed at https://leanprover-community.github.io/mathlib_docs/core/init/algebra/ordered_ring.html#linear_ordered_comm_ring indeed suggests we have nothing like this.
Last updated: May 09 2021 at 10:11 UTC