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 = ⋯

instance instStarModuleNNRealOfReal {E : Type u_1} [AddCommMonoid E] [Star E] [Module ℝ E] [StarModule ℝ E] : StarModule NNReal E

Equations

• ⋯ = ⋯