proposition: Corollary Vandet_VanprodE : Vandet = Vanprod.
proof: Proof. Proof using. rewrite /Vandet Vanmx_antimE. suff -> : antim [::] = antim (0%MM : 'X_{1..n}). by rewrite -alt_detE add0m Vanprod_alt. by apply/matrixP => i j; rewrite !mxE nth_nil -mnm_nth mnm0E. 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)