ℝ and ℝ≥0 are *-ordered rings.

instance Real.instStarOrderedRing : StarOrderedRing ℝ

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.lean.

instance NNReal.instStarOrderedRing : StarOrderedRing NNReal

instance instSelfAdjointDecomposeOfAddLeftMono {R : Type u_1} [AddGroup R] [Lattice R] [AddLeftMono R] [Star R] : SelfAdjointDecompose R