gcommSemiring — Mathlib

English

The family of homogeneous submodules {homogeneousSubmodule(σ, R, i)} forms a graded monoid under multiplication, with 1 in degree 0 and the product of degrees i and j landing in degree i+j.

Русский

Свойство: множество однородных подмодулей {homogeneousSubmodule(σ, R, i)} образует градуированное моноидальное умножение: единица имеет степень 0, а произведение степеней i и j принадлежит степени i+j.

LaTeX

$$$1 \\in homogeneousSubmodule\\ σ\\ R\\ 0 \\quad\\land\\quad homogeneousSubmodule\\ σ\\ R\\ i \\cdot homogeneousSubmodule\\ σ\\ R\\ j \\subseteq homogeneousSubmodule\\ σ\\ R\\ (i+j)$$$

Lean4

/-- The homogeneous submodules form a graded ring. This instance is used by `DirectSum.commSemiring`
and `DirectSum.algebra`. -/
instance gcommSemiring : SetLike.GradedMonoid (homogeneousSubmodule σ R)
    where
  one_mem := isHomogeneous_one σ R
  mul_mem _ _ _ _ := IsHomogeneous.mul

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