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.
