English
Orthogonality of characters for irreducibles: the normalized sum χ_V(g) χ_W(g^{-1}) equals 1 if V ≅ W and 0 otherwise.
Русский
Ортогональность характеров для неразложимых: нормализованная сумма χ_V(g) χ_W(g^{-1}) равна 1, если V ≅ W, и 0 иначе.
LaTeX
$$$\frac{1}{|G|} \sum_{g \in G} \chi_V(g) \chi_W(g^{-1}) = \begin{cases}1 & \text{если } V \cong W \\ 0 & \text{иначе} \end{cases}$$$
Lean4
/-- Orthogonality of characters for irreducible representations of finite group over an
algebraically closed field whose characteristic doesn't divide the order of the group. -/
theorem char_orthonormal (V W : FDRep k G) [Simple V] [Simple W] :
⅟(Fintype.card G : k) • ∑ g : G, V.character g * W.character g⁻¹ = if Nonempty (V ≅ W) then ↑1 else ↑0 :=
by
rw [scalar_product_char_eq_finrank_equivariant]
-- The scalar products of the characters is equal to the dimension of the space of
-- equivariant maps `W ⟶ V`.
rw_mod_cast [finrank_hom_simple_simple W V, Iso.nonempty_iso_symm]
-- By Schur's Lemma, the dimension of `Hom_G(W, V)` is `1` is `V ≅ W` and `0` otherwise.
