instFiniteElemSubtypeMemSubgroupClosureCommutatorRepresentativesCommutatorSet

English

The commutator set of the closure of representatives is finite: Finite (commutatorSet (closureCommutatorRepresentatives(G))).

Русский

Множество коммутаторов замыкания представителей конечно.

LaTeX

$$$\mathrm{Finite}(\mathrm{commutatorSet}(\mathrm{closureCommutatorRepresentatives}(G)))$$$

Lean4

instance : Finite (commutatorSet (closureCommutatorRepresentatives G)) :=
  by
  apply Nat.finite_of_card_ne_zero
  rw [card_commutatorSet_closureCommutatorRepresentatives]
  exact Finite.card_pos.ne'

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