instMonoidFG — 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 monoids is finitely generated. -/
@[to_additive /-- Finite product of finitely generated additive monoids is finitely generated. -/
    ]
instance instMonoidFG {M : ι → Type*} [∀ i, Monoid (M i)] [∀ i, Monoid.FG (M i)] : Monoid.FG (∀ i, M i) where
  fg_top := by
    rw [← Submonoid.pi_top Set.univ]
    exact .pi fun i => Monoid.FG.fg_top

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