iff_add_fg — Mathlib

English

A finitely generated group G is equivalent to the corresponding additive group Additive G being finitely generated.

Русский

Пусть G — порожденная группа; тогда Additive G порожден как аддитивная группа эквивалентно этому.

LaTeX

$$$\operatorname{FG}(G) \iff \operatorname{AddGroup.FG}(\operatorname{Additive} G)$$$

Lean4

theorem iff_add_fg : Group.FG G ↔ AddGroup.FG (Additive G) :=
  ⟨fun h => ⟨(Subgroup.fg_iff_add_fg ⊤).1 h.out⟩, fun h => ⟨(Subgroup.fg_iff_add_fg ⊤).2 h.out⟩⟩

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