proposition: Lemma mxminpoly_uconj n (V : 'M[F]_(n.+1)) (f : 'M_n.+1) : V \in unitmx -> mxminpoly (conjmx V f) = mxminpoly f.
proof: Proof. have simp := (row_free_unit, stablemx_unit, unitmx_inv, unitmx1). move=> Vu; apply/eqP; rewrite -eqp_monic ?mxminpoly_monic// /eqp. apply/andP; split; first by rewrite mxminpoly_conj ?simp. by rewrite -[f in X in X %| _](conjmxK _ Vu) mxminpoly_conj ?simp. 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)