no goals
R : Type u_2
M : Type ?u.721203
inst✝³ : CommMonoid M
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ FiniteType R (MonoidAlgebra R G) ↔ Group.FG G
simpa [Group.fg_iff_monoid_fg] using finiteType_iff_fg