proposition: Lemma det_trmx : forall n (A : 'M_n), \det A^T === \det A.
proof: Proof. move=> n A; pose r := 'I_n; pose ip p : 'S_n := p^-1%g. rewrite /(\det _). setoid_rewrite (reindex (h:=ip)) at 1 => /=; last first. by exists ip => s _; rewrite /ip invgK. apply eq_bigr => s _; rewrite !odd_permV /=. apply rmul_morph; first by reflexivity. setoid_rewrite (reindex (h:=s)) at 1. apply eq_bigr => i _; rewrite permK /trmx; reflexivity. by exists (s^-1%g : _ -> _) => i _; rewrite ?permK ?permKV. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms