proposition: Lemma Lemma3 K d : Eigen1Vec K d -> forall r, CommonEigenVec K d r.+1.
proof: Proof. move=> E1V_K_d; elim=> [|r IHr m V]; first exact/Eigen1VecP. move: (\rank V) {-2}V (leqnn (\rank V)) => n {V}. elim: n m => [|n IHn] m V. by rewrite leqn0 => /eqP ->; rewrite dvdn0. move=> le_rV_Sn HrV [] // f sf /= [] ssf f_sf_stabV f_sf_comm. have [->|f_neq0] := altP (f =P 0). have [||v v_neq0 Hsf] := (IHr _ _ HrV _ ssf). + by move=> g f_sf /=; rewrite f_sf_stabV // in_cons f_sf orbT. + move=> g h g_sf h_sf /=. by apply: f_sf_comm; rewrite !in_cons ?g_sf ?h_sf ?orbT. exists v => // g; rewrite in_cons => /orP [/eqP->|]; last exact: Hsf. by exists 0; apply/eigenspaceP; rewrite mulmx0 scale0r. have f_stabV : (V *m f <= V)%MS by rewrite f_sf_stabV ?mem_head. have sf_stabV : {in sf, forall f, (V *m f <= V)%MS}. by move=> g g_sf /=; rewrite f_sf_stabV // in_cons g_sf orbT. pose f' := restrict V f; pose sf' := map (restrict V) sf. have [||a a_eigen_f'] := E1V_K_d _ 1%:M _ f'; do ?by rewrite ?mxrank1 ?submx1. pose W := (eigenspace f' a)%MS; pose Z := (f' - a%:M). have rWZ : (\rank W + \rank Z)%N = \rank V. by rewrite (mxrank_ker (f' - a%:M)) subnK // rank_leq_row. have f'_stabW : (W *m f' <= W)%MS. by rewrite (eigenspaceP (submx_refl _)) scalemx_sub. have f'_stabZ : (Z *m f' <= Z)%MS. rewrite (submx_trans _ (submxMl f' _)) //. by rewrite mulmxDl mulmxDr mulmxN mulNmx scalar_mxC. have sf'_comm : {in [::f' & sf'] &, forall f g, f *m g = g *m f}. move=> g' h' /=; rewrite -!map_cons. move=> /mapP [g g_s_sf -> {g'}] /mapP [h h_s_sf -> {h'}]. by rewrite -!restrictM ?inE /= ?f_sf_stabV // f_sf_comm. have sf'_stabW : {in sf', forall f, (W *m f <= W)%MS}. move=> g g_sf /=; apply/eigenspaceP. rewrite -mulmxA -[g *m _]sf'_comm ?(mem_head, in_cons, g_sf, orbT) //. by rewrite mulmxA scalemxAl (eigenspaceP (submx_refl _)). have sf'_stabZ : {in sf', forall f, (Z *m f <= Z)%MS}. move=> g g_sf /=. rewrite mulmxBl sf'_comm ?(mem_head, in_cons, g_sf, orbT) //. by rewrite -scalar_mxC -mulmxBr submxMl. have [eqWV|neqWV] := altP (@eqmxP _ _ _ _ W 1%:M). have [] // := IHr _ W _ sf'; do ?by rewrite ?eqWV ?mxrank1 ?size_map. move=> g h g_sf' h_sf'; apply: sf'_comm; by rewrite in_cons (g_sf', h_sf') orbT. move=> v v_neq0 Hv; exists (v *m row_base V). by rewrite mul_mx_rowfree_eq0 ?row_base_free. move=> g; rewrite in_cons => /orP [/eqP ->|g_sf]; last first. have [|b] := Hv (restrict V g); first by rewrite map_f. by rewrite eigenspace_restrict // ?sf_stabV //; exists b. by exists a; rewrite -eigenspace_restrict // eqWV submx1. have lt_WV : (\rank W < \rank V)%N. rewrite -[X in (_ < X)%N](@mxrank1 K) rank_ltmx //. by rewrite ltmxEneq neqWV // submx1. have ltZV : (\rank Z < \rank V)%N. rewrite -[X in (_ < X)%N]rWZ -subn_gt0 addnK lt0n mxrank_eq0 -lt0mx. move: a_eigen_f' => /eigenvalueP [v /eigenspaceP] sub_vW v_neq0. by rewrite (ltmx_sub_trans _ sub_vW) // lt0mx. have [] // := IHn _ (if d %| \rank Z then W else Z) _ _ [:: f' & sf']. + by rewrite -ltnS (@leq_trans (\rank V)) //; case: ifP. + by apply: contra HrV; case: ifP => [*|-> //]; rewrite -rWZ dvdn_add. + by rewrite /= size_map ssf. + move=> g; rewrite in_cons => /= /orP [/eqP -> {g}|g_sf']; case: ifP => _ //; by rewrite (sf'_stabW, sf'_stabZ). move=> v v_neq0 Hv; exists (v *m row_base V). by rewrite mul_mx_rowfree_eq0 ?row_base_free. move=> g Hg; have [|b] := Hv (restrict V g); first by rewrite -map_cons map_f. rewrite eigenspace_restrict //; first by exists b. by move: Hg; rewrite in_cons => /orP [/eqP -> //|/sf_stabV]. 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)