proposition: Lemma char_diag_block_mx s (F : forall n, nat -> 'M[R]_n.+1) : s != [::] -> char_poly_mx (diag_block_mx s F) = diag_block_mx s (fun n i => char_poly_mx (F n i)).
proof: Proof. case: s=> //= a l _. elim: l a F=> //= b l IHl a F. by rewrite -IHl -char_block_mx. 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