proposition: Lemma diagonalizablePeigen {n} {A : 'M[F]_n} : diagonalizable A <-> exists2 rs, uniq rs & (\sum_(r <- rs) eigenspace A r :=: 1%:M)%MS.
proof: Proof. split=> [df|[rs urs rsP]]. suff [rs rsP] : exists rs, (\sum_(r <- rs) eigenspace A r :=: 1%:M)%MS. exists (undup rs); rewrite ?undup_uniq//; apply: eqmx_trans rsP. elim: rs => //= r rs IHrs; rewrite big_cons. case: ifPn => in_rs; rewrite ?big_cons; last exact: adds_eqmx. apply/(eqmx_trans IHrs)/eqmx_sym/addsmx_idPr. have rrs : (index r rs < size rs)%N by rewrite index_mem. rewrite (big_nth 0) big_mkord (sumsmx_sup (Ordinal rrs)) ?nth_index//. move: df => [P Punit /(diagonalizable_forLR Punit)[d ->]]. exists [seq d 0 i | i <- enum 'I_n]; rewrite big_image/=. apply: (@eqmx_trans _ _ _ _ _ _ P); apply/eqmxP; rewrite ?sub1mx ?submx1 ?row_full_unit//. rewrite submx_full ?row_full_unit//=. apply/row_subP => i; rewrite rowE (sumsmx_sup i)//. apply/eigenspaceP; rewrite conjVmx// !mulmxA mulmxK//. by rewrite -rowE row_diag_mx scalemxAl. have mxdirect_eigenspaces : mxdirect (\sum_(i < size rs) eigenspace A rs`_i). apply: mxdirect_sum_eigenspace => i j _ _ rsij; apply/val_inj. by apply: uniqP rsij; rewrite ?inE. rewrite (big_nth 0) big_mkord in rsP; rewrite -codiagonalizable1. apply/(codiagonalizable_on _ mxdirect_eigenspaces) => // i/=. case: n => [|n] in A {mxdirect_eigenspaces} rsP *. by rewrite thinmx0 sub0mx. by rewrite comm_mx_stable_eigenspace. rewrite codiagonalizable1. by rewrite (@conjmx_eigenvalue _ _ _ rs`_i) ?eq_row_base ?row_base_free. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(div fintype tuple finfun bigop fingroup perm) mathcomp(ssralg zmodp matrix mxalgebra poly polydiv)