proposition: Lemma char_poly_det : char_poly`_0 = (- 1) ^+ n * \det A.
proof: Proof. rewrite big_distrr coef_sum [0%N]lock /=; apply: eq_bigr => s _. rewrite -{1}rmorphN -rmorphXn mul_polyC coefZ /=. rewrite mulrA -exprD addnC exprD -mulrA -lock; congr (_ * _). transitivity (\prod_(i < n) - A i (s i)); last by rewrite prodrN card_ord. elim: (index_enum _) => [|i e IHe]; rewrite !(big_nil, big_cons) ?coef1 //. by rewrite coefM big_ord1 IHe !mxE coefB coefC coefMn coefX mul0rn sub0r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(div fintype tuple finfun bigop fingroup perm) mathcomp(ssralg zmodp matrix mxalgebra poly polydiv)