fg_range — Mathlib

English

If G is finitely generated and f: G → G' is a group homomorphism, then the range f(G) is finitely generated.

Русский

Пусть G конечно порождена; тогда образ f(G) также конечно порожден.

LaTeX

$$$\operatorname{FG}(G) \Rightarrow \operatorname{FG}(\operatorname{range}(f))$$$

Lean4

@[to_additive]
instance fg_range {G' : Type*} [Group G'] [Group.FG G] (f : G →* G') : Group.FG f.range :=
  Group.fg_of_surjective f.rangeRestrict_surjective

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