English
A group G is finitely generated if and only if it is finitely generated as a monoid.
Русский
Группа G конечно порождена тогда и только тогда, когда она конечно порождена как моноид.
LaTeX
$$$\operatorname{FG}(G) \iff \operatorname{Monoid.FG}(G)$$$
Lean4
/-- A group is finitely generated if and only if it is finitely generated as a monoid. -/
@[to_additive /-- An additive group is finitely generated if and only
if it is finitely generated as an additive monoid. -/
]
theorem fg_iff_monoid_fg : Group.FG G ↔ Monoid.FG G :=
⟨fun h => Monoid.fg_def.2 <| (Subgroup.fg_iff_submonoid_fg ⊤).1 (Group.fg_def.1 h), fun h =>
Group.fg_def.2 <| (Subgroup.fg_iff_submonoid_fg ⊤).2 (Monoid.fg_def.1 h)⟩
