proposition: Lemma eigenvalue_root_min a : eigenvalue A a = root p_A a.
proof: Proof. apply/idP/idP=> Aa; last first. rewrite eigenvalue_root_char !root_factor_theorem in Aa *. exact: dvdp_trans Aa mxminpoly_dvd_char. have{Aa} [v Av_av v_nz] := eigenvalueP Aa. apply: contraR v_nz => pa_nz; rewrite -{pa_nz}(eqmx_eq0 (eqmx_scale _ pa_nz)). apply/eqP; rewrite -(mulmx0 _ v) -mx_root_minpoly. elim/poly_ind: p_A => [|p c IHp]. by rewrite rmorph0 horner0 scale0r mulmx0. rewrite !hornerE rmorphD rmorphM /= horner_mx_X horner_mx_C scalerDl. by rewrite -scalerA mulmxDr mul_mx_scalar mulmxA -IHp -scalemxAl Av_av. 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)