instFiniteSubtypeMemCommutatorOfElemCommutatorSet

English

If the commutator set is finite, then the commutator subgroup is finite.

Русский

Если множество коммутаторов конечное, то коммутаторная подгруппа конечна.

LaTeX

$$Finite(card(commutator G)) → Finite(commutator G)$$

Lean4

/-- A theorem of Schur: A group with finitely many commutators has finite commutator subgroup. -/
instance [Finite (commutatorSet G)] : Finite (_root_.commutator G) :=
  by
  have h2 := card_commutator_dvd_index_center_pow (closureCommutatorRepresentatives G)
  refine Nat.finite_of_card_ne_zero fun h => ?_
  rw [card_commutator_closureCommutatorRepresentatives, h, zero_dvd_iff] at h2
  exact FiniteIndex.index_ne_zero (pow_eq_zero h2)

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