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

instance instStarRingReal : StarRing ℝ

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

Equations

• instStarRingReal = starRingOfComm

instance instTrivialStarReal : TrivialStar ℝ

Equations

• instTrivialStarReal = ⋯