fg_iff_submonoid_fg — Mathlib

English

For a submonoid N of a monoid M, N is finitely generated as a monoid if and only if N is finitely generated as a submonoid of M.

Русский

Для подмонойда N под моноидом M условие: N конечно порожден как моноид эквивалентно тому, что N конечно порожден как подмонойд внутри M.

LaTeX

$$$\forall N : Submonoid M, Monoid.FG N \iff N.FG$$$

Lean4

@[to_additive (attr := simp)]
theorem fg_iff_submonoid_fg (N : Submonoid M) : Monoid.FG N ↔ N.FG :=
  by
  conv_rhs => rw [← N.mrange_subtype, MonoidHom.mrange_eq_map]
  exact ⟨fun h ↦ h.fg_top.map N.subtype, fun h => ⟨h.map_injective N.subtype Subtype.coe_injective⟩⟩

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