English
If R is a ring, then RingQuot r inherits a ring structure.
Русский
Если R — кольцо, то RingQuot r наследует кольцевую структуру.
LaTeX
$$$\operatorname{Ring}(\mathrm{Quot}(R,r))$$$
Lean4
instance instRing {R : Type uR} [Ring R] (r : R → R → Prop) : Ring (RingQuot r) :=
{ RingQuot.instSemiring r with
neg := Neg.neg
neg_add_cancel := by
rintro ⟨⟨⟩⟩
simp [neg_quot, add_quot, ← zero_quot]
sub := Sub.sub
sub_eq_add_neg := by
rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩
simp [neg_quot, sub_quot, add_quot, sub_eq_add_neg]
zsmul := (· • ·)
zsmul_zero' := by
rintro ⟨⟨⟩⟩
simp [smul_quot, ← zero_quot]
zsmul_succ' := by
rintro n ⟨⟨⟩⟩
simp [smul_quot, add_quot, add_mul, add_comm]
zsmul_neg' := by
rintro n ⟨⟨⟩⟩
simp [smul_quot, neg_quot, add_mul]
intCast := intCast r
intCast_ofNat := fun n => congrArg RingQuot.mk <| by exact congrArg (Quot.mk _) (Int.cast_natCast _)
intCast_negSucc := fun n =>
congrArg RingQuot.mk <| by
simp_rw [neg_def]
exact congrArg (Quot.mk _) (Int.cast_negSucc n) }
