fg_range — Mathlib

English

If M is finitely generated and f: M →* M' is a monoid hom, then the range of f is finitely generated.

Русский

Если M конечно порожден и f: M →* M' — гомоморфизм моноидов, то образ f является конечнопорожденным.

LaTeX

$$$\forall f : M \rightarrow* M', [Monoid.FG M] \Rightarrow Monoid.FG (MonoidHom.mrange f)$$$

Lean4

@[to_additive]
instance fg_range {M' : Type*} [Monoid M'] [Monoid.FG M] (f : M →* M') : Monoid.FG (MonoidHom.mrange f) :=
  Monoid.fg_of_surjective f.mrangeRestrict f.mrangeRestrict_surjective

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