proposition: Lemma mxminpoly_conj m n (V : 'M[F]_(m.+1, n.+1)) (f : 'M_n.+1) : row_free V -> stablemx V f -> mxminpoly (conjmx V f) %| mxminpoly f.
proof: Proof. by move=> *; rewrite mxminpoly_min// horner_mx_conj// mx_root_minpoly conjmx0. 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)