proposition: Lemma Eigen1VecP (K : fieldType) (d : nat) : CommonEigenVec K d 1%N <-> Eigen1Vec K d.
proof: Proof. split=> [Hd m V HV f|Hd m V HV [] // f [] // _ /(_ _ (mem_head _ _))] f_stabV. have [] := Hd _ _ HV [::f] (erefl _). + by move=> ?; rewrite in_cons orbF => /eqP ->. + by move=> ? ?; rewrite /= !in_cons !orbF => /eqP -> /eqP ->. move=> v v_neq0 /(_ f (mem_head _ _)) [a /eigenspaceP]. by exists a; apply/eigenvalueP; exists v. have [a /eigenvalueP [v /eigenspaceP v_eigen v_neq0]] := Hd _ _ HV _ f_stabV. by exists v => // ?; rewrite in_cons orbF => /eqP ->; exists a. Qed.
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)