proposition: Fact in_homsym_is_linear : linear in_homsym.
proof: Proof. rewrite /in_homsym => a u v. rewrite linear_sum /= -big_split /=; apply eq_bigr => la _. by rewrite scalerA -scalerDl mcoeffD mcoeffZ. 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