closure_finite_fg — Mathlib

English

For any finite subset s of G, the subgroup generated by s is finitely generated.

Русский

Для любого конечного подмножества s ⊆ G подгруппа, порождаемая s, FG.

LaTeX

$$$\operatorname{FG}(\operatorname{Subgroup.closure}(s))$ for finite s$$

Lean4

@[to_additive]
instance closure_finite_fg (s : Set G) [Finite s] : Group.FG (Subgroup.closure s) :=
  haveI := Fintype.ofFinite s
  s.coe_toFinset ▸ Group.closure_finset_fg s.toFinset

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