Commit 2021-05-11 04:39 8dc848c5
View on Github →feat(ring_theory/finiteness): add finite_type_iff_group_fg (#7569)
We add here a simple modification of monoid_algebra.fg_of_finite_type: a group algebra is of finite type if and only if the group is finitely generated (as group opposed to as monoid).