no goals
R : Type u_2
M : Type ?u.314374
inst✝³ : AddCommMonoid M
G : Type u_1
inst✝² : AddCommGroup G
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ FiniteType R (AddMonoidAlgebra R G) ↔ AddGroup.FG G
simpa [AddGroup.fg_iff_addMonoid_fg] using finiteType_iff_fg