proposition: Lemma perm_mx_vec n (s : 'S_n) (z : 'cV[R]_n) : perm_mx s *m z = \matrix_(i < n, j < 1) z (s i) j.
proof: Proof. apply/colP => i; rewrite !mxE (bigID (pred1 (s i))) /=. rewrite big_pred1_eq {1}/perm_mx !mxE eqxx mul1r (eq_bigr (fun _ => 0)). - by rewrite big_const_seq iter_addr0 addr0. - move=> j; move/negbTE => H. by rewrite !mxE eq_sym H /= mul0r. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) ssr_ext f2