English
The quotient inherits a star-ring structure via a suitable star operation on representatives.
Русский
Квотируемый объект наследует структуру звезды-кольца через соответствующую операцию звезды на представительях.
LaTeX
$$$\\\\starRing r hr$ defines a StarRing on RingQuot r.$$
Lean4
/-- Transfer a star_ring instance through a quotient, if the quotient is invariant to `star` -/
def starRing {R : Type u} [Semiring R] [StarRing R] (r : R → R → Prop) (hr : ∀ a b, r a b → r (star a) (star b)) :
StarRing (RingQuot r) where
star := star' r hr
star_involutive := by
rintro ⟨⟨⟩⟩
simp [star'_quot]
star_mul := by
rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩
simp [star'_quot, mul_quot, star_mul]
star_add := by
rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩
simp [star'_quot, add_quot, star_add]
