proposition: Lemma sym_antisym_char_not2 : n >= 2 -> forall p : {mpoly R[n]}, p \is symmetric -> p \is antisym -> p = 0.
proof: Proof. Proof using Hchar. move=> Hn p /= /issymP Hsym /isantisymP Hanti. move: Hchar; rewrite (char_mpoly n R) => Hchp. pose s := tperm (Ordinal (ltnW Hn)) (Ordinal Hn). have:= Hanti s; rewrite Hsym. rewrite odd_tperm /= => /eqP; rewrite !simplexp -addr_eq0. rewrite -mulr2n -mulr_natr mulf_eq0 => /orP[/eqP-> //|] /= /eqP /= H2. by exfalso; move: Hchp; rewrite negb_and H2 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