gcommSemiring — Mathlib

English

One can lift the gsemiring structure to the direct sum of graded submonoids, giving a graded semiring on the direct sum.

Русский

Можно придать структуру graded semiring прямой сумме градационных подсумм.

LaTeX

$$DirectSum.GSemiring (fun i => A i)$$

Lean4

/-- Build a `DirectSum.GCommSemiring` instance for a collection of additive submonoids. -/
instance gcommSemiring [AddCommMonoid ι] [CommSemiring R] [SetLike σ R] [AddSubmonoidClass σ R] (A : ι → σ)
    [SetLike.GradedMonoid A] : DirectSum.GCommSemiring fun i => A i :=
  { SetLike.gCommMonoid A, SetLike.gsemiring A with }

Похожие утверждения