proposition: Lemma codiagonalizableP n (As : seq 'M[F]_n) : {in As &, forall A B, comm_mx A B} /\ {in As, forall A, diagonalizable A} <-> codiagonalizable As.
proof: Proof. split => [cdAs|[P Punit /allP/= AsD]]/=; last first. split; last by exists P; rewrite // AsD. move=> A B AAs BAs; move=> /(_ _ _)/diagonalizable_forPex/sigW in AsD. have [[dA /simmxLR->//] [dB /simmxLR->//]] := (AsD _ AAs, AsD _ BAs). by rewrite /comm_mx -!conjmxM 1?diag_mxC// inE stablemx_unit ?unitmx_inv. move: cdAs; rewrite (rwP (all_comm_mxP _)) => cdAs. have [k] := ubnP (size As); elim: k => [|k IHk]//= in n As cdAs *. case: As cdAs => [|A As]//=; first by exists 1%:M; rewrite ?unitmx1. rewrite ltnS all_comm_mx_cons => -[/andP[/allP/(_ _ _)/eqP AAsC AsC dAAs]] Ask. have /diagonalizablePeigen [rs urs rs1] := dAAs _ (mem_head _ _). rewrite (big_nth 0) big_mkord in rs1. have eAB (i : 'I_(size rs)) B : B \in A :: As -> stablemx (eigenspace A rs`_i) B. case: n => [|n'] in B A As AAsC AsC {dAAs rs1 Ask} * => B_AAs. by rewrite thinmx0 sub0mx. rewrite comm_mx_stable_eigenspace//. by move: B_AAs; rewrite !inE => /predU1P [->//|/AAsC]. apply/(@codiagonalizable_on _ _ _ (_ :: _) rs1) => [|i|i /=]. - apply: mxdirect_sum_eigenspace => i j _ _ rsij; apply/val_inj. by apply: uniqP rsij; rewrite ?inE. - by apply/allP => B B_AAs; rewrite eAB. rewrite (@conjmx_eigenvalue _ _ _ rs`_i) ?eq_row_base ?row_base_free//. set Bs := map _ _; suff [P Punit /= PBs] : codiagonalizable Bs. exists P; rewrite /= ?PBs ?andbT// /(diagonalizable_for _ _). by rewrite conjmx_scalar ?mx_scalar_is_diag// row_free_unit. apply: IHk; rewrite ?size_map/= ?ltnS//; split. apply/all_comm_mxP => _ _ /mapP[/= B BAs ->] /mapP[/= h hAs ->]. rewrite -!conjmxM ?inE ?stablemx_row_base ?eAB ?inE ?BAs ?hAs ?orbT//. by rewrite (all_comm_mxP _ AsC). move=> _ /mapP[/= B BAs ->]. have: stablemx (row_base (eigenspace A rs`_i)) B. by rewrite stablemx_row_base eAB// inE BAs orbT. have := dAAs B; rewrite inE BAs orbT => /(_ isT) [P Punit]. move=> /diagonalizable_forPex[D /(simmxLR Punit)->] sePD. have rAeP : row_free (row_base (eigenspace A rs`_i) *m invmx P). by rewrite /row_free mxrankMfree ?row_free_unit ?unitmx_inv// eq_row_base. rewrite -conjMumx ?unitmx_inv ?row_base_free => [|//|//|//]. apply/diagonalizable_conj_diag => //. by rewrite stablemx_comp// stablemx_unit ?unitmx_inv. 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)