proposition: Lemma expand_det_row n (A : 'M[R]_n) i0 : \det A = \sum_j A i0 j * cofactor A i0 j.
proof: Proof. rewrite /(\det A) (partition_big (fun s : 'S_n => s i0) predT) //=. apply: eq_bigr => j0 _; rewrite expand_cofactor big_distrr /=. apply: eq_bigr => s /eqP Dsi0. rewrite mulrCA (bigID (pred1 i0)) /= big_pred1_eq Dsi0; congr (_ * (_ * _)). by apply: eq_bigl => i; rewrite eq_sym. 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)