average_char_eq_finrank_invariants

English

For a finite group G, the average of the character over G equals the dimension of the invariants: (1/|G|) Σ_g χ(g) = finrank(invariants ρ).

Русский

Для конечной группы G среднее по группе характеристики равно размерности пространства инвариантов: \frac{1}{|G|} \sum_g χ(g) = finrank(инвариантов ρ).

LaTeX

$$$\frac{1}{|G|} \sum_{g \in G} \chi_V(g) = \operatorname{finrank}_k(\operatorname{invariants}\ V.\rho).$$$

Lean4

theorem average_char_eq_finrank_invariants (V : FDRep k G) :
    ⅟(Fintype.card G : k) • ∑ g : G, V.character g = finrank k (invariants V.ρ) :=
  by
  rw [← (isProj_averageMap V.ρ).trace]
  simp [character, GroupAlgebra.average, _root_.map_sum]

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