proposition: Lemma char_poly_trace : n > 0 -> char_poly`_n.-1 = - \tr A.
proof: Proof. move=> n_gt0; have [q <- lt_q_n] := split_diagA; set p := \prod_(x <- _) _. rewrite coefD {q lt_q_n}(nth_default 0 lt_q_n) addr0. have{n_gt0} ->: p`_n.-1 = ('X * p)`_n by rewrite coefXM eqn0Ngt n_gt0. have ->: \tr A = \sum_(x <- diagA) x by rewrite big_map big_filter. rewrite -size_diagA {}/p; elim: diagA => [|x d IHd]. by rewrite !big_nil mulr1 coefX oppr0. rewrite !big_cons coefXM mulrBl coefB IHd opprD addrC; congr (- _ + _). rewrite mul_polyC coefZ [size _]/= -(size_prod_XsubC _ id) -lead_coefE. by rewrite (monicP _) ?monic_prod_XsubC ?mulr1. 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)