fact: Definition Eigen1Vec_def K (phK : phant K) (d : nat) := forall (m : nat) (V : 'M[K]_m), ~~ (d %| \rank V) -> forall (f : 'M_m), (V *m f <= V)%MS -> exists a, eigenvalue f a.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrint div ssrnum rat poly closed_field) mathcomp(polyrcf matrix mxalgebra tuple mxpoly zmodp binomial realalg) mathcomp(mxpoly)