Orthonormality of the Jacobi–Trudi characters

The Jacobi–Trudi characters are orthonormal for the class inner product of the symmetric group, which is what makes them the irreducible characters.

theorem RS.jtChar_orthonormal (μ : YoungDiagram) : (↑μ.card.factorial)⁻¹ * ∑ π : Equiv.Perm (Fin μ.card), jtChar μ π * jtChar μ π = 1

The Jacobi–Trudi characters are of unit norm for the class inner product — which is what makes them irreducible characters.