proposition: Lemma det_diag_block s (F : forall n, nat -> 'M[R]_n.+1) : s != [::] -> \det (diag_block_mx s F) = \prod_(i < size s) \det (F (nth 0%N s i) i).
proof: Proof. case: s=> // n s _. elim: s n F=>[n F|a l IHl n F] /=. by rewrite big_ord_recl big_ord0 mulr1 /=. by rewrite (det_ublock (F n 0%N)) big_ord_recl IHl. 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