gradedMonoid — Mathlib

English

The family of weighted homogeneous submodules forms a graded monoid under submodule multiplication with unit in degree 0.

Русский

Семейство взвешенно однородных подмодулей образует градиентный моноид по умножению подмодулей, единица в степени 0.

LaTeX

$$SetLike.GradedMonoid (weightedHomogeneousSubmodule R w)$$

Lean4

/-- The weighted homogeneous submodules form a graded monoid. -/
theorem gradedMonoid {w : σ → M} : SetLike.GradedMonoid (weightedHomogeneousSubmodule R w)
    where
  one_mem := isWeightedHomogeneous_one R w
  mul_mem _ _ _ _ := IsWeightedHomogeneous.mul

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