closure_finset_fg — Mathlib

English

The closure of a Finset in a monoid is finitely generated.

Русский

Замыкание конечного множества в моноиде является конечнопорожденным.

LaTeX

$$$\forall s : Finset M, Monoid.FG (Submonoid.closure (s : Set M))$$$

Lean4

@[to_additive]
instance closure_finset_fg (s : Finset M) : Monoid.FG (Submonoid.closure (s : Set M)) :=
  by
  refine ⟨⟨s.preimage Subtype.val Subtype.coe_injective.injOn, ?_⟩⟩
  rw [Finset.coe_preimage, Submonoid.closure_closure_coe_preimage]

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