Documentation

Mathlib.Data.Real.StarOrdered

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.

Equations