fg_iff_add_fg — Mathlib

English

A monoid is finitely generated iff its additive version is finitely generated.

Русский

Моноид конечнопорожден тогда и только тогда, когда соответствующий аддитивный моноид также конечнопорожден.

LaTeX

$$$\\forall M,\\; Monoid.FG\, M \\iff AddMonoid.FG\\,(Additive\\,M)$$$

Lean4

theorem fg_iff_add_fg : Monoid.FG M ↔ AddMonoid.FG (Additive M)
    where
  mp _ := ⟨(Submonoid.fg_iff_add_fg ⊤).1 FG.fg_top⟩
  mpr h := ⟨(Submonoid.fg_iff_add_fg ⊤).2 h.fg_top⟩

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