gradedMonoid — Mathlib

English

An instance of gradedMonoid for gradeBy is provided by the identity map.

Русский

Дано экземпляр градуированного моноида для gradeBy, заданный тождественным отображением.

LaTeX

$$$\\text{gradeBy.gradedMonoid} (\\text{id})$$$

Lean4

instance gradedMonoid [AddMonoid M] [CommSemiring R] : SetLike.GradedMonoid (grade R : M → Submodule R R[M]) := by
  apply gradeBy.gradedMonoid (AddMonoidHom.id _)

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