instFintypeAbelianizationOfDecidablePredMemSubgroupCommutator

English

If G is finite and there is a decidable predicate detecting membership in the commutator, then the abelianization G^{ab} is finite.

Русский

Если G конечно по объему и имеется разрешимый предикат принадлежности к коммутатору, то абелизация G^{ab} конечна.

LaTeX

$$$ [Fintype\,G] \Rightarrow Fintype(Abelianization\,G). $$$

Lean4

instance [Fintype G] [DecidablePred (· ∈ commutator G)] : Fintype (Abelianization G) :=
  QuotientGroup.fintype (commutator G)

Похожие утверждения