Commit 2021-04-26 13:34 35b9d9c4
View on Github →feat(group_theory/finiteness): add submonoid.fg (#7279)
I introduce here the notion of a finitely generated monoid (not necessarily commutative) and I prove that the notion is preserved by additive/multiplicative.
A natural continuation is of course to introduce the same notion for groups.