proposition: Lemma companionmxK {R : comRingType} (p : {poly R}) : p \is monic -> char_poly (companionmx p) = p.
proof: Proof. pose D n : 'M[{poly R}]_n := \matrix_(i, j) ('X *+ (i == j.+1 :> nat) - ((i == j)%:R)%:P). have detD n : \det (D n) = (-1) ^+ n. elim: n => [|n IHn]; first by rewrite det_mx00. rewrite (expand_det_row _ ord0) big_ord_recl !mxE /= sub0r. rewrite big1 ?addr0; last by move=> i _; rewrite !mxE /= subrr mul0r. rewrite /cofactor mul1r [X in \det X](_ : _ = D _) ?IHn ?exprS//. by apply/matrixP=> i j; rewrite !mxE /= /bump !add1n eqSS. elim/poly_ind: p => [|p c IHp]. by rewrite monicE lead_coef0 eq_sym oner_eq0. have [->|p_neq0] := eqVneq p 0. rewrite mul0r add0r monicE lead_coefC => /eqP->. by rewrite /companionmx /char_poly size_poly1 det_mx00. rewrite monicE lead_coefDl ?lead_coefMX => [p_monic|]; last first. rewrite size_polyC size_mulX ?polyX_eq0// ltnS. by rewrite (leq_trans (leq_b1 _)) ?size_poly_gt0. rewrite -[in RHS]IHp // /companionmx size_MXaddC (negPf p_neq0) /=. rewrite /char_poly polySpred //. have [->|spV1_gt0] := posnP (size p).-1. rewrite [X in \det X]mx11_scalar det_scalar1 !mxE ?eqxx det_mx00. by rewrite mul1r -horner_coef0 hornerMXaddC mulr0 add0r rmorphN opprK. rewrite (expand_det_col _ ord0) /= -[(size p).-1]prednK //. rewrite big_ord_recr big_ord_recl/= big1 ?add0r //=; last first. move=> i _; rewrite !mxE -val_eqE /= /bump leq0n add1n eqSS. by rewrite ltn_eqF ?subrr ?mul0r. rewrite !mxE ?subnn -horner_coef0 /= hornerMXaddC. rewrite !(eqxx, mulr0, add0r, addr0, subr0, rmorphN, opprK)/=. rewrite mulrC /cofactor; congr (_ * 'X + _). rewrite /cofactor -signr_odd oddD addbb mul1r; congr (\det _). apply/matrixP => i j; rewrite !mxE -val_eqE coefD coefMX coefC. by rewrite /= /bump /= !add1n !eqSS addr0. rewrite /cofactor [X in \det X](_ : _ = D _). by rewrite detD /= addn0 -signr_odd -signr_addb addbb mulr1. apply/matrixP=> i j; rewrite !mxE -!val_eqE /= /bump /=. by rewrite leqNgt ltn_ord add0n add1n [_ == _.-2.+1]ltn_eqF. 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)