Documentation

Mathlib.GroupTheory.MonoidLocalization.Finite

Localization of a finitely generated submonoid #

TODO #

If Mathlib.GroupTheory.Finiteness wasn't so heavy, this could move earlier.

source
theorem Localization.fg {M : Type u_1} [CommMonoid M] {S : Submonoid M} [Monoid.FG M] (hS : S.FG) :
Monoid.FG (Localization S)

The localization of a finitely generated monoid at a finitely generated submonoid is finitely generated.

source
theorem AddLocalization.fg {M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} [AddMonoid.FG M] (hS : S.FG) :
AddMonoid.FG (AddLocalization S)

The localization of a finitely generated monoid at a finitely generated submonoid is finitely generated.

source
instance Algebra.GrothendieckGroup.instFG {M : Type u_1} [CommMonoid M] [Monoid.FG M] :
Monoid.FG (GrothendieckGroup M)

The Grothendieck group of a finitely generated monoid is finitely generated.

source
instance Algebra.GrothendieckAddGroup.instFG {M : Type u_1} [AddCommMonoid M] [AddMonoid.FG M] :
AddMonoid.FG (GrothendieckAddGroup M)

The Grothendieck group of a finitely generated monoid is finitely generated.