proposition: Lemma mcoeff_symm_pol sh m : (symm_pol sh)@_m = (perm_eq sh m)%:R.
proof: Proof. rewrite linear_sum /=. case: (boolP (perm_eq sh m)) => /= [| /(elimN idP)] Hperm. - rewrite (bigD1 (Permuted Hperm)) //= (_ : [multinom m] = m); last exact: val_inj. rewrite mcoeffX eq_refl /= big1 ?addr0 // => p /eqP Hp. rewrite mcoeffX; case: (_ =P _) => //= Heq. by exfalso; apply: Hp; apply val_inj; rewrite /= -Heq. - rewrite big1 // => p _. rewrite mcoeffX; case: (_ =P _) => //= Heq. by exfalso; apply Hperm; rewrite -Heq /=; exact: permutedP. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm) mathcomp(ssrcomplements freeg mpoly) sorted tools ordtype permuted partition skewpart composition Yamanouchi std tableau stdtab skewtab permcent antisym Schur_mpoly therule Schur_altdef unitriginv