fact: Definition CommonEigenVec_def K (phK : phant K) (d r : nat) := forall (m : nat) (V : 'M[K]_m), ~~ (d %| \rank V) -> forall (sf : seq 'M_m), size sf = r -> {in sf, forall f, (V *m f <= V)%MS} -> {in sf &, forall f g, f *m g = g *m f} -> exists2 v : 'rV_m, (v != 0) & forall f, f \in sf -> exists a, (v <= eigenspace f a)%MS.
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)