proposition: Lemma expand_cofactor n (A : 'M[R]_n) i j : cofactor A i j = \sum_(s : 'S_n | s i == j) (-1) ^+ s * \prod_(k | i != k) A k (s k).
proof: Proof. case: n A i j => [|n] A i0 j0; first by case: i0. rewrite (reindex (lift_perm i0 j0)); last first. pose ulsf i (s : 'S_n.+1) k := odflt k (unlift (s i) (s (lift i k))). have ulsfK i (s : 'S_n.+1) k: lift (s i) (ulsf i s k) = s (lift i k). rewrite /ulsf; have:= neq_lift i k. by rewrite -(can_eq (permK s)) => /unlift_some[] ? ? ->. have inj_ulsf: injective (ulsf i0 _). move=> s; apply: can_inj (ulsf (s i0) s^-1%g) _ => k'. by rewrite {1}/ulsf ulsfK !permK liftK. exists (fun s => perm (inj_ulsf s)) => [s _ | s]. by apply/permP=> k'; rewrite permE /ulsf lift_perm_lift lift_perm_id liftK. move/(s _ =P _) => si0; apply/permP=> k. case: (unliftP i0 k) => [k'|] ->; rewrite ?lift_perm_id //. by rewrite lift_perm_lift -si0 permE ulsfK. rewrite /cofactor big_distrr /=. apply: eq_big => [s | s _]; first by rewrite lift_perm_id eqxx. rewrite -signr_odd mulrA -signr_addb oddD -odd_lift_perm; congr (_ * _). case: (pickP 'I_n) => [k0 _ | n0]; last first. by rewrite !big1 // => [j /unlift_some[i] | i _]; have:= n0 i. rewrite (reindex (lift i0)). by apply: eq_big => [k | k _] /=; rewrite ?neq_lift // !mxE lift_perm_lift. exists (fun k => odflt k0 (unlift i0 k)) => k; first by rewrite liftK. by case/unlift_some=> k' -> ->. 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)