ℝ
and ℝ≥0
are *-ordered rings. #
Although the instance RCLike.toStarOrderedRing
exists, it is locked behind the
ComplexOrder
scope because currently the order on ℂ
is not enabled globally. But we
want StarOrderedRing ℝ
to be available globally, so we include this instance separately.
In addition, providing this instance here makes it available earlier in the import
hierarchy; otherwise in order to access it we would need to import Mathlib.Analysis.RCLike.Basic
.