English
The direct sum carries a semiring structure induced by the graded semiring A; in particular, addition and multiplication are defined componentwise via the graded monoid.
Русский
Прямая сумма обладает структурой полугруппы-полуполосения, индуцированной градуированной полугруппой A; операция сложения и умножения по координатам задаются через градуированную моноидную структуру.
LaTeX
$$$\text{Semiring}(\bigoplus_i A_i)$$$
Lean4
/-- The `Semiring` structure derived from `GSemiring A`. -/
instance semiring : Semiring (⨁ i, A i) :=
{
(inferInstance : NonUnitalNonAssocSemiring
_) with
one_mul := one_mul A
mul_one := mul_one A
mul_assoc := mul_assoc A
toNatCast := instNatCast _
natCast_zero := by simp only [NatCast.natCast, GSemiring.natCast_zero, map_zero]
natCast_succ := fun n => by
simp_rw [NatCast.natCast, GSemiring.natCast_succ]
rw [map_add]
rfl }
