*-ring structure on ℚ and ℚ≥0.

@[instance_reducible]

instance Rat.instStarRing : StarRing ℚ

Equations

• Rat.instStarRing = starRingOfComm

@[instance_reducible]

instance NNRat.instStarRing : StarRing ℚ≥0

Equations

• NNRat.instStarRing = starRingOfComm

instance Rat.instTrivialStar : TrivialStar ℚ

instance NNRat.instTrivialStar : TrivialStar ℚ≥0

@[simp]

theorem star_nnratCast {R : Type u_1} [DivisionSemiring R] [StarRing R] (q : ℚ≥0) : star ↑q = ↑q

@[simp]

theorem star_ratCast {R : Type u_1} [DivisionRing R] [StarRing R] (r : ℚ) : star ↑r = ↑r