proposition: Lemma irrSG_orthonormal la mu : '['irrSG[la], 'irrSG[mu]] = (la == mu)%:R.
proof: Proof. by rewrite /irrSG Fchar_inv_isometry // homsymdotss. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism gproduct) mathcomp(rat ssralg ssrint ssrnum algC vector archimedean) mathcomp(mxrepresentation classfun character) mathcomp(mpoly) sorted ordtype tools partition antisym sympoly homogsym Cauchy Schur_altdef stdtab therule permcomp cycletype towerSn permcent reprSn unitriginv MurnaghanNakayama