proposition: Lemma diag_block_mx_seq s (F : forall n, nat -> 'M_n.+1) : let n := size_sum s in let l := mkseq (fun i => (F 0%N i) ord0 ord0) (size s) in (forall i, nth 0%N s i = 0%N) -> diag_block_mx s F = diag_mx_seq n.+1 n.+1 l.
proof: Proof. move=> /= Hs. set s1 := mkseq _ _. have ->: s = nseq (size s1) 0%N. apply: (@eq_from_nth _ 0%N); first by rewrite size_mkseq size_nseq. by move=> i Hi; rewrite Hs nth_nseq size_mkseq Hi. rewrite diag_mx_seq_block. apply: ext_block=> i; rewrite size_nseq size_mkseq => Hi. rewrite nth_nseq Hi nth_mkseq //. by apply/matrixP=> k l; rewrite !mxE !ord1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm poly mxpoly finfun tuple) mathcomp(matrix bigop zmodp polydiv) ssrcomplements dvdring