proposition: Lemma det_tr n (A : 'M[R]_n) : \det A^T = \det A.
proof: Proof. rewrite [\det A^T](reindex_inj invg_inj) /=. apply: eq_bigr => s _ /=; rewrite !odd_permV (reindex_perm s) /=. by congr (_ * _); apply: eq_bigr => i _; rewrite mxE permK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg countalg finalg zmodp)