proposition: Lemma eigenspace_restrict f : (V *m f <= V)%MS -> forall n a (W : 'M_(n, \rank V)), (W <= eigenspace (restrict f) a)%MS = (W *m row_base V <= eigenspace f a)%MS.
proof: Proof. move=> f_stabV n a W; apply/eigenspaceP/eigenspaceP; rewrite scalemxAl. by move<-; rewrite -mulmxA -[X in _ = X]mulmxA mulmxKpV ?stable_row_base. move/(congr1 (mulmx^~ (pinvmx (row_base V)))). rewrite -2!mulmxA [_ *m (f *m _)]mulmxA => ->. by apply: (row_free_inj (row_base_free V)); rewrite mulmxKpV ?submxMl. 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)