proposition: Lemma det_perm_mx : forall n (s : 'S_n), \det (perm_mx s) === (-(1:R)) ^+s.
proof: Proof. move=> n s; rewrite /(\det _); setoid_rewrite (bigD1 (j:=s))=>//=. setoid_rewrite (big1 (I:=perm_for_finType (ordinal_finType n))). rewrite/perm_mx; setoid_rewrite (big1 (I:=ordinal_finType n)); first by ring. by move=> i _; rewrite eq_refl; reflexivity. move=> t neq; rewrite/perm_mx. have Heq : req (\prod_(i < n) (if s i == t i then 1 else 0)) 0; last by rewrite -> Heq; ring. case: (pickP (fun i => s i != t i)) => [i ist | Est]. by setoid_rewrite (bigD1 (j:=i))=>//; rewrite (negbTE ist); ring. by case/eqP:neq; apply/permP=>i; apply/eqP; move:(Est i); rewrite eq_sym; apply negbFE. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms