proposition: Lemma char_poly_monic : char_poly \is monic.
proof: Proof. rewrite monicE -(monicP (monic_prod_XsubC diagA xpredT id)). rewrite !lead_coefE size_char_poly. have [q <- lt_q_n] := split_diagA; have le_q_n := leq_trans lt_q_n (leq_pred n). by rewrite size_prod_XsubC size_diagA coefD (nth_default 0 le_q_n) addr0. 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)