proposition: Lemma expand_cofactor : forall n (A : 'M_n) i j, cofactor A i j === \sum_(s : 'S_n | s i == j) (-(1:R)) ^+ s * \prod_(k | i != k) A k (s k).
proof: Proof. move=> [_ [] //|n] A i0 j0; setoid_rewrite (reindex (h:=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: forall i (s : 'S__) k, lift (s i) (ulsf i s k) = s (lift i k). rewrite /ulsf => i s k; have:= neq_lift i k. by rewrite -(inj_eq (@perm_inj _ s)); case/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 /determinant. setoid_rewrite (big_distrr (I:=perm_for_finType (ordinal_finType (predn (S n)))))=> /=. apply eq_big => [s | s _]; first by rewrite lift_perm_id eqxx. have Heq : forall i, req ((-rI) ^+ i) ((-rI) ^+ (odd i)). elim=>[|i]//=; first by reflexivity. by case: (odd i)=>/= H; simpl; ring_simplify; rewrite -> H; ring. rewrite -> Heq, odd_lift_perm, <- odd_add, (Rmul_assoc r_rt). apply rmul_morph; first by case: (odd (i0 + j0)); case (odd_perm s)=>//=; ring. case: (pickP 'I_n) => [k0 _ | n0]; last first. setoid_rewrite (big1 (I:=ordinal_finType n))=>[|i _]; last by have:= n0 i. setoid_rewrite (big1 (I:=ordinal_finType (S n)))=>[|j]; first by reflexivity. by case/unlift_some=> i; have:= n0 i. setoid_rewrite (reindex (h:=lift i0)). apply eq_big => [k | k _] /=; first by rewrite neq_lift //. by rewrite lift_perm_lift; reflexivity. exists (fun k => odflt k0 (unlift i0 k)) => k; first by rewrite liftK. by case/unlift_some=> k' -> ->. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms