proposition: Lemma expand_det_col : forall n (A : 'M_n) j0, \det A === \sum_i (A i j0 * cofactor A i j0).
proof: Proof. move=> n A j0; rewrite <- det_trmx, (expand_det_row _ j0). by apply eq_bigr => i _; rewrite -> cofactor_tr; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms