two_mul_nat_card_alternatingGroup

English

For nontrivial α, 2 · card(Alt(α)) = card(Perm(α)).

Русский

Для ненулевого α выполняется 2 · |Alt(α)| = |Perm(α)|.

LaTeX

$$$2 \cdot \operatorname{card}(\mathrm{alternatingGroup}(\alpha)) = \operatorname{card}(\mathrm{Perm}(\alpha))$$$

Lean4

theorem two_mul_nat_card_alternatingGroup [Nontrivial α] : 2 * Nat.card (alternatingGroup α) = Nat.card (Perm α) := by
  simp only [← alternatingGroup.index_eq_two (α := α), index_mul_card]

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