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)

theorem RingQuot.star'_quot {R : Type u} [Semiring R] (r : R → R → Prop) [StarRing R] (hr : ∀ (a b : R), r a b → r (star a) (star b)) {a : R} : RingQuot.star'✝ r hr { toQuot := Quot.mk (Rel r) a } = { toQuot := Quot.mk (Rel r) (star a) }

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 star_ring instance through a quotient, if the quotient is invariant to star

Equations

• RingQuot.starRing r hr = StarRing.mk ⋯