proposition: Lemma Kostka_unitrig (R : comUnitRingType) d : unitrig (fun la mu : 'PDom_d => 'K(la, mu)%:R : R).
proof: Proof. apply/unitrigP; split => [la | la mu]. - by rewrite Kostka_diag. - by apply contraR => /Kostka0 ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm) mathcomp(mpoly) tools combclass ordtype sorted partition tableau skewpart skewtab antisym Schur_mpoly freeSchur therule std stdtab unitriginv presentSn