proposition: Lemma row'_col'_char_poly_mx {R : ringType} m i (M : 'M[R]_m) : row' i (col' i (char_poly_mx M)) = char_poly_mx (row' i (col' i M)).
proof: Proof. by apply/matrixP => k l; rewrite !mxE (inj_eq lift_inj). 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)