proposition: Lemma simmx_minpoly {n} {P A B : 'M[F]_n.+1} : P \in unitmx -> A ~_P B -> mxminpoly A = mxminpoly B.
proof: Proof. by move=> Pu /eqP<-; rewrite mxminpoly_uconj. 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)