rank_commutator_le_card — Mathlib

English

The rank of the commutator subgroup of G is bounded above by the cardinality of the set of commutators in G: rank(commutator G) ≤ card(commutatorSet G).

Русский

Раnk коммутаторной подгруппы G ограничен мощностью множества коммутаторов commutatorSet(G).

LaTeX

$$$ \\operatorname{rank}(\\operatorname{commutator}(G)) \\le |\\operatorname{commutatorSet}(G)| $$$

Lean4

theorem rank_commutator_le_card : Group.rank (_root_.commutator G) ≤ Nat.card (commutatorSet G) :=
  by
  rw [Subgroup.rank_congr (commutator_eq_closure G)]
  apply Subgroup.rank_closure_finite_le_nat_card

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