fg_iff_mul_fg — Mathlib

English

For an Additive Monoid M, Finite Generation of M as an AddMonoid is equivalent to Finite Generation of Multiplicative M.

Русский

Для аддитивного моноида M конечнопорожденность M как AddMonoid эквивалентна конечнопорожденности как Multiplicative M.

LaTeX

$$$\\forall M\\; [AddMonoid M] : AddMonoid.FG M \\iff Monoid.FG (Multiplicative M)$$$

Lean4

theorem fg_iff_mul_fg {M : Type*} [AddMonoid M] : AddMonoid.FG M ↔ Monoid.FG (Multiplicative M)
    where
  mp _ := ⟨(AddSubmonoid.fg_iff_mul_fg ⊤).1 FG.fg_top⟩
  mpr h := ⟨(AddSubmonoid.fg_iff_mul_fg ⊤).2 h.fg_top⟩

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