card_eq_sum_card_group_div_card_stabilizer

English

A finite version of the class formula: the size of β equals the sum over orbits of |G| divided by stabilizers.

Русский

Дискретная версия формулы классов: размер β равен сумме по орбитам |G| деленное на стабилизаторы.

LaTeX

$$$|\beta| = \sum_{\omega} \frac{|G|}{|\operatorname{stabilizer}(G,\omega)|}$$$

Lean4

/-- **Class formula** for a finite group acting on a finite type. -/
@[to_additive /-- **Class formula** for a finite group acting on a finite type. -/
    ]
theorem card_eq_sum_card_group_div_card_stabilizer [Fintype α] [Fintype β] [Fintype Ω]
    [∀ b : β, Fintype <| stabilizer α b] :
    Fintype.card β = ∑ ω : Ω, Fintype.card α / Fintype.card (stabilizer α ω.out) :=
  card_eq_sum_card_group_div_card_stabilizer' α β Quotient.out_eq'

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