proposition: Lemma det0P n (A : 'M[R]_n) : reflect (exists2 v : 'rV[R]_n, v != 0 & v *m A = 0) (\det A == 0).
proof: Proof. apply: (iffP eqP) => [detA0 | [v n0v vA0]]; last first. apply: contraNeq n0v => nz_detA; rewrite -(inj_eq (scalemx_inj nz_detA)). by rewrite scaler0 -mul_mx_scalar -mul_mx_adj mulmxA vA0 mul0mx. elim: n => [|n IHn] in A detA0 *. by case/idP: (oner_eq0 R); rewrite -detA0 [A]thinmx0 -(thinmx0 1%:M) det1. have [{detA0}A'0 | nzA'] := eqVneq (row 0 (\adj A)) 0; last first. exists (row 0 (\adj A)) => //; rewrite rowE -mulmxA mul_adj_mx detA0. by rewrite mul_mx_scalar scale0r. pose A' := col' 0 A; pose vA := col 0 A. have defA: A = row_mx vA A'. apply/matrixP=> i j /[!mxE]. by case: split_ordP => j' -> /[!(mxE, ord1)]; congr (A i _); apply: val_inj. have{IHn} w_ j : exists w : 'rV_n.+1, [/\ w != 0, w 0 j = 0 & w *m A' = 0]. have [|wj nzwj wjA'0] := IHn (row' j A'). by apply/eqP; move/rowP/(_ j)/eqP: A'0; rewrite !mxE mulf_eq0 signr_eq0. exists (\row_k oapp (wj 0) 0 (unlift j k)). rewrite !mxE unlift_none -wjA'0; split=> //. apply: contraNneq nzwj => w0; apply/eqP/rowP=> k'. by move/rowP/(_ (lift j k')): w0; rewrite !mxE liftK. apply/rowP=> k; rewrite !mxE (bigD1_ord j) //= mxE unlift_none mul0r add0r. by apply: eq_big => //= k'; rewrite !mxE/= liftK. have [w0 [/rV0Pn[j nz_w0j] w00_0 w0A']] := w_ 0; pose a0 := (w0 *m vA) 0 0. have{w_} [wj [nz_wj wj0_0 wjA']] := w_ j; pose aj := (wj *m vA) 0 0. have [aj0 | nz_aj] := eqVneq aj 0. exists wj => //; rewrite defA (@mul_mx_row _ _ _ 1) [_ *m _]mx11_scalar -/aj. by rewrite aj0 raddf0 wjA' row_mx0. exists (aj *: w0 - a0 *: wj). apply: contraNneq nz_aj; move/rowP/(_ j)/eqP; rewrite !mxE wj0_0 mulr0 subr0. by rewrite mulf_eq0 (negPf nz_w0j) orbF. rewrite defA (@mul_mx_row _ _ _ 1) !mulmxBl -!scalemxAl w0A' wjA' !linear0. by rewrite -mul_mx_scalar -mul_scalar_mx -!mx11_scalar subrr addr0 row_mx0. 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)