proposition: Lemma eigenvalue_conjmx V f : stablemx V f -> row_free V -> {subset eigenvalue (conjmx V f) <= eigenvalue f}.
proof: Proof. by move=> fV rfV a; rewrite ![_ \in _]eigenvalue_poly; apply: eigenpoly_conjmx. 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)