The non-negative real numbers are a *-ring, with the trivial *-structure

instance instStarRingNNReal : StarRing NNReal

Equations

• instStarRingNNReal = starRingOfComm

instance instTrivialStarNNReal : TrivialStar NNReal

Equations

• instTrivialStarNNReal = ⋯

instance instStarModuleNNRealReal : StarModule NNReal ℝ

Equations

• instStarModuleNNRealReal = ⋯