proposition: Lemma symbhE la : ('hh)`_(enum_rank la) = 'hh[la] :> HSF.
proof: Proof. by rewrite /symbh tupleE /= (nth_map la) ?nth_enum_rank // -cardE. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg matrix vector ssrnum algC archimedean) mathcomp(fingroup perm) mathcomp(ssrcomplements freeg mpoly) tools sorted ordtype permuted partition permcent antisym Schur_mpoly Schur_altdef sympoly