English
RingQuot r carries an additive commutative monoid structure induced by addition in the base ring.
Русский
RingQuot r обладает аддитивной коммутативной полугруппой с нулём, наследуемой от сложения в R.
LaTeX
$$$[a] + [b] = [b] + [a]$$$
Lean4
instance instAddCommMonoid (r : R → R → Prop) : AddCommMonoid (RingQuot r)
where
add := (· + ·)
zero := 0
add_assoc := by
rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩ ⟨⟨⟩⟩
simp only [add_quot, add_assoc]
zero_add := by
rintro ⟨⟨⟩⟩
simp [add_quot, ← zero_quot, zero_add]
add_zero := by
rintro ⟨⟨⟩⟩
simp only [add_quot, ← zero_quot, add_zero]
add_comm := by
rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩
simp only [add_quot, add_comm]
nsmul := (· • ·)
nsmul_zero := by
rintro ⟨⟨⟩⟩
simp only [smul_quot, zero_smul, zero_quot]
nsmul_succ := by
rintro n ⟨⟨⟩⟩
simp only [smul_quot, nsmul_eq_mul, Nat.cast_add, Nat.cast_one, add_mul, one_mul, add_comm, add_quot]
