of — Mathlib · SciLib

English

The inclusion map of a commutative monoid M into its Grothendieck group GrothendieckGroup M is a monoid homomorphism.

Русский

Включение из коммутативного моноида M в его группу Гротендик GrothendieckGroup M является гомоморфизмом моноидов.

LaTeX

$$$\\mathrm{of}: M \\to \\mathrm{GrothendieckGroup}(M)$ is a monoid homomorphism$$

Lean4

/-- The inclusion from a commutative monoid `M` to its Grothendieck group.

Note that this is only injective if `M` is cancellative. -/
@[to_additive /-- The inclusion from an additive commutative monoid `M` to its Grothendieck group.

    Note that this is only injective if `M` is cancellative. -/
    ]
abbrev of : M →* GrothendieckGroup M :=
  (monoidOf ⊤).toMonoidHom

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