single_mem_grade — Mathlib

English

The collection gradeBy R f i forms a graded monoid under the additive monoid structure, compatible with multiplication.

Русский

Коллекция gradeBy R f i образует градуированный моноид, совместимый с операцией умножения.

LaTeX

$$$\\text{gradeBy} \\; R\\; f\\; :\\ ι \\to\\ Submodule\\; R\\; R[M] \\quad \\text{одна } \\text{monoid graded structure}$$$

Lean4

theorem single_mem_grade {R} [CommSemiring R] (i : M) (r : R) : Finsupp.single i r ∈ grade R i :=
  single_mem_gradeBy _ _ _

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