← Mathematical handbook

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

@[instance_reducible]

instance instStarRingNNReal : StarRing NNReal

Equations

• instStarRingNNReal = starRingOfComm

instance instTrivialStarNNReal : TrivialStar NNReal

instance instStarModuleNNRealReal : StarModule NNReal ℝ

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