Theorem Monoid.fg_iff_add_fg

Modification history

2026-09-15 15:39
Mathlib/GroupTheory/Finiteness.lean
feat(GroupTheory/Finiteness): add general `IsMulFG` (#43532) …
Modified Monoid.fg_iff_add_fgView on Github →
2025-04-03 18:22
Mathlib/GroupTheory/Finiteness.lean
feat: the product of finitely generated monoids is finitely generated (#22932) …
Modified Monoid.fg_iff_add_fgView on Github →
2023-05-16 06:36
Mathlib/GroupTheory/Finiteness.lean
refactor: rename `Fg` to `FG` (#3948) …
Modified Monoid.fg_iff_add_fgView on Github →
2023-02-11 15:55
Mathlib/GroupTheory/Finiteness.lean
feat Port/GroupTheory.Finiteness (#2187)
Added Monoid.fg_iff_add_fgView on Github →