fg_iff_mul_fg — Mathlib

English

Finitely generated additive subgroups are equivalent to finitely generated as multiplicative subgroups.

Русский

Конечнопорожденность как AddSubgroup равна FG как Subgroup в мультипликативной форме.

LaTeX

$$$\forall P : AddSubgroup H, P.FG \iff P.toSubgroup.FG$$$

Lean4

theorem fg_iff_mul_fg (P : AddSubgroup H) : P.FG ↔ P.toSubgroup.FG :=
  by
  rw [AddSubgroup.fg_iff_addSubmonoid_fg, Subgroup.fg_iff_submonoid_fg]
  exact AddSubmonoid.fg_iff_mul_fg (AddSubgroup.toAddSubmonoid P)

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