fg_iff_mul_fg — Mathlib

English

An additive group on H is finitely generated iff the multiplicative group on H is finitely generated.

Русский

Аддитивная группа на H порождена кончно тогда, когда мультипликативная группа на H порождена кончно.

LaTeX

$$$\operatorname{AddGroup.FG}(H) \iff \operatorname{FG}(\operatorname{Multiplicative} H)$$$

Lean4

theorem fg_iff_mul_fg : AddGroup.FG H ↔ Group.FG (Multiplicative H) :=
  ⟨fun h => ⟨(AddSubgroup.fg_iff_mul_fg ⊤).1 h.out⟩, fun h => ⟨(AddSubgroup.fg_iff_mul_fg ⊤).2 h.out⟩⟩

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