proposition: Lemma conjmx_eigenvalue a V f : (V <= eigenspace f a)%MS -> row_free V -> conjmx V f = a%:M.
proof: Proof. by move=> /eigenspaceP Vfa rfV; rewrite /conjmx Vfa -mul_scalar_mx mulmxKp. 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)