mathlib

4722dd46 - feat(ring_theory/finiteness): add add_monoid_algebra.ft_of_fg (#7265)

feat(ring_theory/finiteness): add add_monoid_algebra.ft_of_fg (#7265) This is from `lean_liquid`. We prove `add_monoid_algebra.ft_of_fg`: if `M` is a finitely generated monoid then `add_monoid_algebra R M` if finitely generated as `R-alg`. The converse is also true, but the proof is longer and I wanted to keep the PR small. - [x] depends on: #7279