proposition: Lemma similar_mxminpoly m' n' (A : 'M[R]_m'.+1) (B : 'M[R]_n'.+1) : similar A B -> mxminpoly A = mxminpoly B.
proof: Proof. move=> HAB; apply/eqP; rewrite -eqp_monic //; try exact: mxminpoly_monic. apply/andP; split; apply: mxminpoly_min. by apply/(similar_horner (similar_sym HAB))/mx_root_minpoly. by apply/(similar_horner HAB)/mx_root_minpoly. 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