proposition: Lemma eigenvalue_root_char (F : fieldType) n (A : 'M[F]_n) a : eigenvalue A a = root (char_poly A) a.
proof: Proof. transitivity (\det (a%:M - A) == 0). apply/eigenvalueP/det0P=> [[v Av_av v_nz] | [v v_nz Av_av]]; exists v => //. by rewrite mulmxBr Av_av mul_mx_scalar subrr. by apply/eqP; rewrite -mul_mx_scalar eq_sym -subr_eq0 -mulmxBr Av_av. congr (_ == 0); rewrite horner_sum; apply: eq_bigr => s _. rewrite hornerM horner_exp !hornerE; congr (_ * _). rewrite (big_morph _ (fun p q => hornerM p q a) (hornerC 1 a)). by apply: eq_bigr => i _; rewrite !mxE !(hornerE, hornerMn). 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)