proposition: Lemma char_mpoly n (R : ringType) : [char R] =i [char {mpoly R[n]}].
proof: Proof. Proof using. move=> p; rewrite !unfold_in /= -mpolyC_nat. case: (prime.prime p) => //=. apply/eqP/eqP => [-> //|]. rewrite -(mpolyP) => /(_ 0%MM). by rewrite mcoeff0 raddfMn /= mcoeffMn mcoeff1 eq_refl /= => ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition