proposition: Lemma vec_perm_mx n (s : 'S_n) (z : 'rV[R]_n) : z *m perm_mx s = \matrix_(i < 1, j < n) z i ((s^-1)%g j).
proof: Proof. apply/rowP => j; rewrite !mxE (bigID (pred1 ((s^-1)%g j))) /=. rewrite big_pred1_eq !mxE {2}permE perm_invK eqxx mulr1 (eq_bigr (fun _ => 0)). - by rewrite big_const_seq iter_addr0 addr0. - move=> i H. rewrite !mxE (_ : (s i == j) = false); first by rewrite mulr0. apply/eqP; move/eqP in H; contradict H. by rewrite -H -permM (mulgV s) perm1. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) ssr_ext f2