Missing instance

Stream: maths

[Yury G. Kudryashov]

Am I right that we have no linear_ordered_field → linear_ordered_comm_ring instance?

[Patrick Massot]

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.