proposition: Lemma char_block_mx 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. apply/matrixP=> i j; rewrite !mxE. case: splitP=> k Hk; rewrite !mxE; case: splitP=> l Hl; rewrite !mxE; rewrite -!(inj_eq (@ord_inj _)) Hk Hl ?subr0 ?eqn_add2l //. by rewrite ltn_eqF // ltn_addr. by rewrite gtn_eqF // ltn_addr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype finfun perm matrix bigop zmodp mxalgebra) mathcomp(choice poly polydiv mxpoly binomial)