proposition: Lemma eigenvalue_restrict f : (V *m f <= V)%MS -> {subset eigenvalue (restrict f) <= eigenvalue f}.
proof: Proof. move=> f_stabV a /eigenvalueP [x /eigenspaceP]; rewrite eigenspace_restrict //. move=> /eigenspaceP Hf x_neq0; apply/eigenvalueP. by exists (x *m row_base V); rewrite ?mul_mx_rowfree_eq0 ?row_base_free. 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)