English
RingQuot r carries a semiring structure induced by the base semiring R.
Русский
RingQuot r наследует структуру полуправильного кольца, порождаемую базовым полуправильным кольцом R.
LaTeX
$$$\operatorname{Semiring}(\mathrm{Quot}(R,r))$$$
Lean4
instance instSemiring (r : R → R → Prop) : Semiring (RingQuot r)
where
natCast := natCast r
natCast_zero := by simp [Nat.cast, natCast, ← zero_quot]
natCast_succ := by simp [Nat.cast, natCast, ← one_quot, add_quot]
left_distrib := by
rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩ ⟨⟨⟩⟩
simp only [mul_quot, add_quot, left_distrib]
right_distrib := by
rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩ ⟨⟨⟩⟩
simp only [mul_quot, add_quot, right_distrib]
nsmul := (· • ·)
nsmul_zero := by
rintro ⟨⟨⟩⟩
simp only [zero_smul]
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]
__ := instAddCommMonoid r
__ := instMonoidWithZero r
