closure_finset_fg — Mathlib

English

Finite product of finitely generated monoids is finitely generated.

Русский

Конечная произвольная прямая сумма (произведение) FG моноидов FG.

LaTeX

$$$\operatorname{FG}(M_i)\;\text{for all } i \Rightarrow \operatorname{FG}\left(\prod_i M_i\right)$$$

Lean4

@[to_additive]
instance closure_finset_fg (s : Finset G) : Group.FG (Subgroup.closure (s : Set G)) :=
  by
  refine ⟨⟨s.preimage Subtype.val Subtype.coe_injective.injOn, ?_⟩⟩
  rw [Finset.coe_preimage, ← Subgroup.coe_subtype, Subgroup.closure_preimage_eq_top]

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