proposition: Lemma char_block_diag_mx {R : ringType} m n (A : 'M[R]_m) (B : 'M[R]_n) : char_poly_mx (block_mx A 0 0 B) = block_mx (char_poly_mx A) 0 0 (char_poly_mx B).
proof: Proof. rewrite /char_poly_mx map_block_mx/= !map_mx0. by rewrite scalar_mx_block opp_block_mx add_block_mx !subr0. 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)