mathlib

251a42b5 - feat(ring_theory/finiteness): add monoid_algebra.ft_iff_fg (#7445)

feat(ring_theory/finiteness): add monoid_algebra.ft_iff_fg (#7445) We prove here `add monoid_algebra.ft_iff_fg`: the monoid algebra is of finite type if and only if the monoid is finitely generated. - [x] depends on: #7409