English
If the commutator set is finite, the commutator subgroup is bounded by cardCommutatorBound of the commutator set size.
Русский
Если множество коммутаторов конечно, размер коммутаторной подгруппы не превышает cardCommutatorBound(card(commutatorSet G)).
LaTeX
$$Nat.card(_root_.commutator G) ≤ cardCommutatorBound(Nat.card(commutatorSet G))$$
Lean4
/-- A theorem of Schur: The size of the commutator subgroup is bounded in terms of the number of
commutators. -/
theorem card_commutator_le_of_finite_commutatorSet [Finite (commutatorSet G)] :
Nat.card (_root_.commutator G) ≤ cardCommutatorBound (Nat.card (commutatorSet G)) :=
by
have h1 := index_center_le_pow (closureCommutatorRepresentatives G)
have h2 := card_commutator_dvd_index_center_pow (closureCommutatorRepresentatives G)
rw [card_commutatorSet_closureCommutatorRepresentatives] at h1 h2
rw [card_commutator_closureCommutatorRepresentatives] at h2
replace h1 := h1.trans (Nat.pow_le_pow_right Finite.card_pos (rank_closureCommutatorRepresentatives_le G))
replace h2 := h2.trans (pow_dvd_pow _ (add_le_add_right (mul_le_mul_right' h1 _) 1))
rw [← pow_succ] at h2
refine (Nat.le_of_dvd ?_ h2).trans (Nat.pow_le_pow_left h1 _)
exact pow_pos (Nat.pos_of_ne_zero FiniteIndex.index_ne_zero) _
