fact: Definition alternpol n (R : ringType) (f : {mpoly R[n]}) : {mpoly R[n]} := \sum_(s : 'S_n) (-1) ^+ s *: msym s f.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition