proposition: Lemma eigenvalueP a : reflect (exists2 v : 'rV_n, v *m g = a *: v & v != 0) (eigenvalue a).
proof: Proof. by apply: (iffP (rowV0Pn _)) => [] [v]; move/eigenspaceP; exists v. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg finalg zmodp matrix)