proposition: Lemma Lemma6 k r : CommonEigenVec R[i] (2^k.+1) r.+1.
proof: Proof. elim: k {-2}k (leqnn k) r => [|k IHk] l. by rewrite leqn0 => /eqP ->; apply: Lemma3; apply: Lemma5. rewrite leq_eqVlt ltnS => /orP [/eqP ->|/IHk //] r {l}. apply: Lemma3 => m V Hn f f_stabV {r}. have [dvd2n|Ndvd2n] := boolP (2 %| \rank V); last first. exact: @Lemma5 _ _ Ndvd2n _ f_stabV. suff: exists a, eigenvalue (restrict V f) a. by move=> [a /eigenvalue_restrict Hf]; exists a; apply: Hf. case: (\rank V) (restrict V f) => {f f_stabV V m} [|n] f in Hn dvd2n *. by rewrite dvdn0 in Hn. pose L1 := lin_mx [linear of mulmxr f \+ (mulmx f^T)]. pose L2 := lin_mx [linear of mulmxr f \o mulmx f^T]. have [] /= := IHk _ (leqnn _) _ _ (skew R[i] n.+1) _ [::L1; L2] (erefl _). + rewrite rank_skew; apply: contra Hn. rewrite -(@dvdn_pmul2r 2) //= -expnSr muln2 -[_.*2]add0n. have n_odd : odd n by rewrite dvdn2 /= ?negbK in dvd2n *. have {2}<- : odd (n.+1 * n) = 0%N :> nat by rewrite oddM /= andNb. by rewrite odd_double_half Gauss_dvdl // coprime_pexpl // coprime2n. + move=> L; rewrite 2!in_cons in_nil orbF => /orP [] /eqP ->; apply/rV_subP => v /submxP [s -> {v}]; rewrite mulmxA; apply/skewP; set u := _ *m skew _ _; do [have /skewP : (u <= skew R[i] n.+1)%MS by rewrite submxMl]; rewrite mul_rV_lin /= !mxvecK => skew_u. by rewrite opprD linearD /= !trmx_mul skew_u mulmxN mulNmx addrC trmxK. by rewrite !trmx_mul trmxK skew_u mulNmx mulmxN mulmxA. + suff commL1L2: L1 *m L2 = L2 *m L1. move=> La Lb; rewrite !in_cons !in_nil !orbF. by move=> /orP [] /eqP -> /orP [] /eqP -> //; symmetry. apply/eqP/mulmxP => u; rewrite !mulmxA !mul_rV_lin ?mxvecK /=. by rewrite !(mulmxDr, mulmxDl, mulmxA). move=> v v_neq0 HL1L2; have [] := (HL1L2 L1, HL1L2 L2). rewrite !(mem_head, in_cons) orbT => [] [] // a vL1 [] // b vL2 {HL1L2}. move/eigenspaceP in vL1; move/eigenspaceP in vL2. move: vL2 => /(congr1 vec_mx); rewrite linearZ mul_rV_lin /= mxvecK. move: vL1 => /(congr1 vec_mx); rewrite linearZ mul_rV_lin /= mxvecK. move=> /(canRL (addKr _)) ->; rewrite mulmxDl mulNmx => Hv. pose p := 'X^2 + (- a) *: 'X + b%:P. have : vec_mx v *m (horner_mx f p) = 0. rewrite !(rmorphN, rmorphB, rmorphD, rmorphM) /= linearZ /=. rewrite horner_mx_X horner_mx_C !mulmxDr mul_mx_scalar -Hv. rewrite addrAC addrA mulmxA addrN add0r. by rewrite -scalemxAl -scalemxAr scaleNr addrN. rewrite [p]monic_canonical_form; move: (_ / 2%:R) (_ / 2%:R). move=> r2 r1 {Hv p a b L1 L2 Hn}. rewrite rmorphM /= !rmorphB /= horner_mx_X !horner_mx_C mulmxA => Hv. have: exists2 w : 'M_n.+1, w != 0 & exists a, (w <= eigenspace f a)%MS. move: Hv; set w := vec_mx _ *m _. have [w_eq0 _|w_neq0 r2_eigen] := altP (w =P 0). exists (vec_mx v); rewrite ?vec_mx_eq0 //; exists r1. apply/eigenspaceP/eqP. by rewrite -mul_mx_scalar -subr_eq0 -mulmxBr -/w w_eq0. exists w => //; exists r2; apply/eigenspaceP/eqP. by rewrite -mul_mx_scalar -subr_eq0 -mulmxBr r2_eigen. move=> [w w_neq0 [a /(submx_trans (nz_row_sub _)) /eigenspaceP Hw]]. by exists a; apply/eigenvalueP; exists (nz_row w); rewrite ?nz_row_eq0. 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)