instMonoidFG — Mathlib

English

The product of two finitely generated monoids is finitely generated.

Русский

Произведение двух FG моноидов FG.

LaTeX

$$$\operatorname{FG}(M) \land \operatorname{FG}(N) \Rightarrow \operatorname{FG}(M \times N)$$$

Lean4

/-- The product of two finitely generated monoids is finitely generated. -/
@[to_additive /-- The product of two finitely generated additive monoids is finitely generated. -/
    ]
instance instMonoidFG [FG M] [FG N] : FG (M × N) where
  fg_top := by
    rw [← Submonoid.top_prod_top]
    exact ‹FG M›.fg_top.prod ‹FG N›.fg_top

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