proposition: Lemma alt_detE s : 'a_(s + rho) = \det (antim s).
proof: Proof. Proof using. rewrite /alternpol (reindex_inj (inv_inj invgK)) /=; apply eq_bigr => p _. rewrite odd_permV scaler_sign -mulr_sign; congr (_ * _). transitivity (\prod_(i < n) 'X_i ^+ (nth 0%N s (p i) + (n - 1) - p i) : {mpoly R[n]}); first last. by apply eq_bigr => i _; rewrite mxE. rewrite msymX mpolyXE_id; apply eq_bigr => i _; congr (_ ^+ _). rewrite mnmE /= mnmDE invgK mnmE (mnm_nth 0%N) subn1 addnBA //. by rewrite -ltnS (ltn_predK (ltn_ord i)). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition mathcomp(matrix)