The abelianization of a finite group is finite

@[implicit_reducible]

instance instFintypeAbelianizationOfDecidablePredMemSubgroupCommutator {G : Type u_1} [Group G] [Fintype G] [DecidablePred fun (x : G) => x ∈ commutator G] : Fintype (Abelianization G)

instance instFiniteAbelianization {G : Type u_1} [Group G] [Finite G] : Finite (Abelianization G)