card — Mathlib

English

Let N and G be groups and φ: G →* Aut(N) a action of G on N. Then the semidirect product N ⋊_φ G has cardinality equal to the product of the cardinalities of N and G: |N ⋊_φ G| = |N| · |G|.

Русский

Пусть N и G — группы и φ: G →* Aut(N) задаёт действие G на N. Тогда кардинальность полупрямого произведения N ⋊_φ G равна произведению кардинальностей N и G: |N ⋊_φ G| = |N| · |G|.

LaTeX

$$$|N \\rtimes_{\\phi} G| = |N| \\cdot |G|$$$

Lean4

@[simp]
theorem card : Nat.card (N ⋊[φ] G) = Nat.card N * Nat.card G :=
  Nat.card_prod _ _ ▸ Nat.card_congr equivProd

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