proposition: Lemma eigenpoly_conjmx V f : stablemx V f -> row_free V -> {subset eigenpoly (conjmx V f) <= eigenpoly f}.
proof: Proof. move=> fV rfV a /eigenpolyP [x]; rewrite sub_kermxpoly_conjmx//. move=> xV_le_fa x_neq0; apply/eigenpolyP. by exists (x *m V); rewrite ?mulmx_free_eq0. 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)