instGroupFG — Mathlib

English

The product of two finitely generated groups is finitely generated.

Русский

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

LaTeX

$$$\operatorname{FG}(G) \land \operatorname{FG}(H) \Rightarrow \operatorname{FG}(G \times H)$$$

Lean4

/-- The product of two finitely generated groups is finitely generated. -/
@[to_additive /-- The product of two finitely generated additive groups is finitely generated. -/
    ]
instance instGroupFG [FG G] [FG G'] : FG (G × G') where
  out := by
    rw [← Subgroup.top_prod_top]
    exact ‹FG G›.out.prod ‹FG G'›.out

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