instFG — Mathlib

English

If M is finitely generated, then its Grothendieck group GrothendieckGroup M is finitely generated.

Русский

Если моноид M конечносгенерирован, то его группа Гротендика GrothendieckGroup M также конечносгенерирован.

LaTeX

$$$\\text{Monoid.FG }M \\Rightarrow \\text{Monoid.FG}(\\mathrm{GrothendieckGroup}(M))$$$

Lean4

/-- The Grothendieck group of a finitely generated monoid is finitely generated. -/
@[to_additive /-- The Grothendieck group of a finitely generated monoid is finitely generated. -/
    ]
instance instFG [Monoid.FG M] : Monoid.FG <| GrothendieckGroup M :=
  fg Monoid.FG.fg_top

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