instGroupFG — Mathlib

English

Finite product of finitely generated groups is finitely generated.

Русский

Конечное произведение конечно порожденных групп FG.

LaTeX

$$$\operatorname{FG}((i \mapsto G_i))$ for finite ι$$

Lean4

/-- Finite product of finitely generated groups is finitely generated. -/
@[to_additive /-- Finite product of finitely generated additive groups is finitely generated. -/
    ]
instance instGroupFG {G : ι → Type*} [∀ i, Group (G i)] [∀ i, Group.FG (G i)] : Group.FG (∀ i, G i) where
  out := by
    rw [← Subgroup.pi_top Set.univ]
    exact .pi fun i => Group.FG.out

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