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 a) (star b))
⦃a : R⦄
⦃b : R⦄
(h : RingQuot.Rel r a b)
:
RingQuot.Rel r (star a) (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 (RingQuot.Rel r) a } = { toQuot := Quot.mk (RingQuot.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))
:
Transfer a star_ring instance through a quotient, if the quotient is invariant to star
Equations
- RingQuot.starRing r hr = StarRing.mk ⋯