English
RingQuot r forms a monoid with zero under multiplication: multiplication is associative and has a unit, with zero acting as absorbing element.
Русский
RingQuot r образует моноид с нулём относительно умножения: умножение ассоциативно, существует единица, ноль является absorbing элементом.
LaTeX
$$$[a] \cdot [b] = [ab]$$$
Lean4
instance instMonoidWithZero (r : R → R → Prop) : MonoidWithZero (RingQuot r)
where
mul_assoc := by
rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩ ⟨⟨⟩⟩
simp only [mul_quot, mul_assoc]
one_mul := by
rintro ⟨⟨⟩⟩
simp only [mul_quot, ← one_quot, one_mul]
mul_one := by
rintro ⟨⟨⟩⟩
simp only [mul_quot, ← one_quot, mul_one]
zero_mul := by
rintro ⟨⟨⟩⟩
simp only [mul_quot, ← zero_quot, zero_mul]
mul_zero := by
rintro ⟨⟨⟩⟩
simp only [mul_quot, ← zero_quot, mul_zero]
npow n x := x ^ n
npow_zero := by
rintro ⟨⟨⟩⟩
simp only [pow_quot, ← one_quot, pow_zero]
npow_succ := by
rintro n ⟨⟨⟩⟩
simp only [pow_quot, mul_quot, pow_succ]
