proposition: Lemma similar_char_poly m' n' (A : 'M[R]_m') (B : 'M[R]_n') : similar A B -> char_poly A = char_poly B.
proof: Proof. case=> eq [P HP HAB]; rewrite /char_poly /char_poly_mx. have H: map_mx polyC P \in unitmx by rewrite map_unitmx. apply: similar_det; split=> //. rewrite -eq in B HAB *; rewrite conform_mx_id in HAB. exists (map_mx polyC P) => //; rewrite conform_mx_id. by rewrite mulmxDr mulmxDl scalar_mxC mulmxN mulNmx -!map_mxM HAB. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype fintype finfun ssrnat seq) mathcomp(choice ssralg poly polydiv mxpoly matrix bigop) mathcomp(mxalgebra perm fingroup tuple) mxstructure dvdring