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

@[implicit_reducible]

instance instStarRingReal : StarRing ℝ

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

Equations

• instStarRingReal = starRingOfComm

instance instTrivialStarReal : TrivialStar ℝ