English
Let A : ι → σ be a graded monoid structure on a set of subobjects of R. Then the zero-grade component A(0) inherits a commutative semiring structure from R, i.e., A(0) is a commutative semiring with addition and multiplication induced from R.
Русский
Пусть A : ι → σ задаёт градуированную моноиду подмножеств R. Нулевая компонента A(0) наследует от R структуру коммутативного полукольца: A(0) образует коммутативное полукольцо, операции сложения и умножения индуцированы из R.
LaTeX
$$$A_0$ carries a commutative semiring structure induced by the ambient semiring structure on $R$.$$
Lean4
/-- The commutative semiring `A 0` inherited from `R` in the presence of
`SetLike.GradedMonoid A`. -/
instance instCommSemiring : CommSemiring (A 0) :=
(subsemiring A).toCommSemiring
