English
If M is finitely generated and S is a finitely generated submonoid, then Localization S is finitely generated.
Русский
Если M - конечно-сгенерированное, и S - конечно-сгенерированный подмоноид, то Localization S конечно-генерирован.
LaTeX
$$[Monoid.FG M] → Localization FG$$
Lean4
/-- The localization of a finitely generated monoid at a finitely generated submonoid is
finitely generated. -/
@[to_additive /-- The localization of a finitely generated monoid at a finitely generated submonoid
is finitely generated. -/
]
theorem fg [Monoid.FG M] (hS : S.FG) : Monoid.FG <| Localization S := by rw [← Monoid.fg_iff_submonoid_fg] at hS;
exact Monoid.fg_of_surjective mkHom mkHom_surjective
