fg_iff_add_fg — Mathlib

English

A finitely generated subgroup is finitely generated as an additive subgroup; equivalence with the additive counterpart.

Русский

Конечнопорожденная подгруппа эквивалентна конечнопорожденности как AddSubgroup.

LaTeX

$$$\forall P : Subgroup G, P.FG \iff P.toAddSubgroup.FG$$$

Lean4

theorem fg_iff_add_fg (P : Subgroup G) : P.FG ↔ P.toAddSubgroup.FG :=
  by
  rw [Subgroup.fg_iff_submonoid_fg, AddSubgroup.fg_iff_addSubmonoid_fg]
  exact (Subgroup.toSubmonoid P).fg_iff_add_fg

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