proposition: Lemma Lemma4 r : CommonEigenVec R 2 r.+1.
proof: Proof. apply: Lemma3=> m V hV f f_stabV. have [|a] := @odd_poly_root _ (char_poly (restrict V f)). by rewrite size_char_poly /= -dvdn2. rewrite -eigenvalue_root_char => /eigenvalueP [v] /eigenspaceP v_eigen v_neq0. exists a; apply/eigenvalueP; exists (v *m row_base V). by apply/eigenspaceP; rewrite -eigenspace_restrict. by 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)