English
Let M and M' be monoids. If P is a finitely generated submonoid of M and e: M →* M' is a monoid hom, then the image P.map e is a finitely generated submonoid of M'.
Русский
Пусть M и M' — моноиды. Если P — конечнопорожденный подмоноид M, и e: M →* M' — гомоморфизм моноидов, то образ P под e, P.map e, является конечнопорожденным подмоноидом M'.
LaTeX
$$$\forall M M' [Monoid M] [Monoid M'] (P : Submonoid M), P.FG \to \forall e : M \to* M', (P.map e).FG$$$
Lean4
@[to_additive]
theorem map {M' : Type*} [Monoid M'] {P : Submonoid M} (h : P.FG) (e : M →* M') : (P.map e).FG := by
classical
obtain ⟨s, rfl⟩ := h
exact ⟨s.image e, by rw [Finset.coe_image, MonoidHom.map_mclosure]⟩
