proposition: Lemma conjmxM (m n : nat) (V : 'M[F]_(m, n)) : {in [pred f | stablemx V f] &, {morph conjmx V : f g / f *m g}}.
proof: Proof. move=> f g; rewrite !inE => Vf Vg /=. by rewrite /conjmx 2!mulmxA mulmxA mulmxKpV ?stablemx_row_base. 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)