fg_of_surjective — Mathlib

English

If G is finitely generated and f: G →* G' is surjective, then G' is finitely generated.

Русский

Если G порождена кончно и существует сюръективный одоморфизм f: G →* G', то G' тоже порождается кончески.

LaTeX

$$$\text{Group.FG}(G) \land \operatorname{Surjective}(f) \Rightarrow \operatorname{Group.FG}(G')$$$

Lean4

@[to_additive]
theorem fg_of_surjective {G' : Type*} [Group G'] [hG : Group.FG G] {f : G →* G'} (hf : Function.Surjective f) :
    Group.FG G' :=
  Group.fg_iff_monoid_fg.mpr <| @Monoid.fg_of_surjective G _ G' _ (Group.fg_iff_monoid_fg.mp hG) f hf

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