card_commutatorSet_closureCommutatorRepresentatives

English

The number of commutators does not change when passing to the closure of the set of representatives: card(commutatorSet(closureCommutatorRepresentatives(G))) = card(commutatorSet(G)).

Русский

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

LaTeX

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

Lean4

theorem card_commutatorSet_closureCommutatorRepresentatives :
    Nat.card (commutatorSet (closureCommutatorRepresentatives G)) = Nat.card (commutatorSet G) :=
  by
  rw [← image_commutatorSet_closureCommutatorRepresentatives G]
  exact Nat.card_congr (Equiv.Set.image _ _ (subtype_injective _))

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