English
A bound for the commutator subgroup in terms of the center’s index and the commutator set size.
Русский
Ограничение размера коммутаторной подгруппы через индекс центра и размер множества коммутаторов.
LaTeX
$$|commutator G| ∣ (center G).index ^ ((center G).index * card(commutatorSet G) + 1)$$
Lean4
theorem exists_smul_eq (hH : Nat.Coprime (Nat.card H) H.index) (α β : H.QuotientDiff) : ∃ h : H, h • α = β :=
Quotient.inductionOn' α
(Quotient.inductionOn' β fun β α =>
Exists.imp (fun _ => Quotient.sound')
⟨(powCoprime hH).symm (diff (MonoidHom.id H) β α),
(diff_inv _ _ _).symm.trans
(inv_eq_one.mpr
((smul_diff' β α ((powCoprime hH).symm (diff (MonoidHom.id H) β α))⁻¹).trans
(by rw [inv_pow, ← powCoprime_apply hH, Equiv.apply_symm_apply, mul_inv_cancel])))⟩)
