card_orbit_mul_card_stabilizer_eq_card_group

English

If α is finite and the orbit and stabilizer are finite, then |orbit| · |stabilizer| = |G|.

Русский

Если орбита и стабилизатор конечны, то их произведение кардинальностей равно кардинальности группы.

LaTeX

$$Fintype.card(orbit(α,b)) * Fintype.card(stabilizer(α,b)) = Fintype.card(α) $$

Lean4

/-- Orbit-stabilizer theorem. -/
@[to_additive AddAction.card_orbit_mul_card_stabilizer_eq_card_addGroup /-- Orbit-stabilizer theorem. -/
    ]
theorem card_orbit_mul_card_stabilizer_eq_card_group (b : β) [Fintype α] [Fintype <| orbit α b]
    [Fintype <| stabilizer α b] : Fintype.card (orbit α b) * Fintype.card (stabilizer α b) = Fintype.card α := by
  rw [← Fintype.card_prod, Fintype.card_congr (orbitProdStabilizerEquivGroup α b)]

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