The abelianization of a finite group is finite

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

Equations

• instFintypeAbelianizationOfDecidablePredMemSubgroupCommutator = QuotientGroup.fintype (commutator G)

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