proposition: Lemma sub_eigenspace_conjmx V f a W : stablemx V f -> row_free V -> (W <= eigenspace (conjmx V f) a)%MS = (W *m V <= eigenspace f a)%MS.
proof: Proof. by move=> fV rfV; rewrite !eigenspace_poly sub_kermxpoly_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)