proposition: Lemma mul_mx_adj n (A : 'M[R]_n) : A *m \adj A = (\det A)%:M.
proof: Proof. apply/matrixP=> i1 i2 /[!mxE]; have [->|Di] := eqVneq. rewrite (expand_det_row _ i2) //=. by apply: eq_bigr => j _; congr (_ * _); rewrite mxE. pose B := \matrix_(i, j) (if i == i2 then A i1 j else A i j). have EBi12: B i1 =1 B i2 by move=> j; rewrite /= !mxE eqxx (negPf Di). rewrite -[_ *+ _](determinant_alternate Di EBi12) (expand_det_row _ i2). apply: eq_bigr => j _; rewrite !mxE eqxx; congr (_ * (_ * _)). apply: eq_bigr => s _; congr (_ * _); apply: eq_bigr => i _. by rewrite !mxE eq_sym -if_neg neq_lift. 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)