proposition: Lemma submatrix_char_poly_mx m p (M : 'M[R]_m) (f : 'I_p -> 'I_m) (hf : injective f) : submatrix f f (char_poly_mx M) = char_poly_mx (submatrix f f M).
proof: Proof. by rewrite /char_poly_mx -submatrix_map_mx submatrix_sub submatrix_scalar_mx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path ssralg) mathcomp(fintype perm choice finfun matrix bigop zmodp poly mxpoly)