card_commutator_closureCommutatorRepresentatives

English

The number of elements in the commutator of the closure of the representatives equals that of the original group: card(commutator(closureCommutatorRepresentatives(G))) = card(commutator(G)).

Русский

Число элементов коммутатора замыкания представителей равно числу элементов коммутатора исходной группы: card(commutator(closureCommutatorRepresentatives(G))) = card(commutator(G)).

LaTeX

$$$\#\mathrm{commutator}(\mathrm{closureCommutatorRepresentatives}(G)) = \#\mathrm{commutator}(G)$$$

Lean4

theorem card_commutator_closureCommutatorRepresentatives :
    Nat.card (commutator (closureCommutatorRepresentatives G)) = Nat.card (commutator G) :=
  by
  rw [commutator_eq_closure G, ← image_commutatorSet_closureCommutatorRepresentatives, ← MonoidHom.map_closure, ←
    commutator_eq_closure]
  exact Nat.card_congr (Equiv.Set.image _ _ (subtype_injective _))

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