proposition: Lemma expand_det_row : forall n (A : 'M_n) i0, \det A === \sum_j A i0 j * cofactor A i0 j.
proof: Proof. move=> n A i0; rewrite /(\det A). setoid_rewrite (partition_big (P:=predT) (p:=fun s : 'S_n => s i0) (Q:=predT))=>//. apply eq_bigr => j0 _; rewrite -> expand_cofactor. setoid_rewrite (big_distrr _ (A i0 j0)). apply eq_bigr => s; move/eqP=> Dsi0. setoid_rewrite (bigID _ (pred1 i0)) at 1=>/=. setoid_rewrite (big_pred1_eq (I:=ordinal_finType n)). rewrite Dsi0; ring_simplify. apply rmul_morph; first by reflexivity. by apply eq_bigl=>i; rewrite eq_sym. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms