mathlib3

55b3f820 - feat(representation_theory/character): orthogonality of characters (#16043)

feat(representation_theory/character): orthogonality of characters (#16043) Orthogonality of characters for representations of finite groups Co-authored-by: antoinelab01 <66086247+antoinelab01@users.noreply.github.com>