The *-ring structure on suitable quotients of a *-ring.

theorem RingQuot.Rel.star {R : Type u} [Semiring R] (r : R → R → Prop) [StarRing R] (hr : ∀ (a b : R), r a b → r (Star.star a) (Star.star b)) ⦃a b : R⦄ (h : Rel r a b) : Rel r (Star.star a) (Star.star b)

@[instance_reducible]

def RingQuot.starRing {R : Type u} [Semiring R] [StarRing R] (r : R → R → Prop) (hr : ∀ (a b : R), r a b → r (star a) (star b)) : StarRing (RingQuot r)

Transfer a StarRing instance through a quotient, if the quotient is invariant to star

Equations

• RingQuot.starRing r hr = { star := RingQuot.star'✝ r hr, star_involutive := ⋯, star_mul := ⋯, star_add := ⋯ }