proposition: Lemma diagonalizable_for_sum (F : fieldType) (m n : nat) (p_ : 'I_n -> nat) (V_ : forall i, 'M[F]_(p_ i, m)) (A : 'M[F]_m) : mxdirect (\sum_i <<V_ i>>) -> (forall i, stablemx (V_ i) A) -> (forall i, row_free (V_ i)) -> diagonalizable_for (\mxcol_i V_ i) A = [forall i, diagonalizable_for (V_ i) A].
proof: Proof. move=> Vd VA rAV; have aVA : stablemx (\mxcol_i V_ i) A. rewrite (eqmx_stable _ (eqmx_col _)) stablemx_sums//. by move=> i; rewrite (eqmx_stable _ (genmxE _)). apply/diagonalizable_forPex/'forall_diagonalizable_forPex => /= [[D /(simmxPp aVA) +] i|/(_ _)/sigW DoA]. rewrite mxcol_mul -[D]submxrowK diag_mxrow mul_mxdiag_mxcol. move=> /eq_mxcolP/(_ i); set D0 := (submxrow _ _) => VMeq. by exists D0; apply/simmxW. exists (\mxrow_i tag (DoA i)); apply/simmxW. rewrite -row_leq_rank eqmx_col (mxdirectP Vd)/=. by under [leqRHS]eq_bigr do rewrite genmxE (eqP (rAV _)). rewrite mxcol_mul diag_mxrow mul_mxdiag_mxcol; apply: eq_mxcol => i. by case: DoA => /= k /(simmxPp); rewrite VA => /(_ isT) ->. 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)