proposition: Lemma conjMmx (m n p : nat) (V : 'M[F]_(m, n)) (W : 'M_(n, p)) (f : 'M_p) : row_free (V *m W) -> stablemx W f -> stablemx V (conjmx W f) -> conjmx (V *m W) f = conjmx V (conjmx W f).
proof: Proof. move=> rfVW Wf VWf; apply: (row_free_inj rfVW); rewrite mulmxKpV ?stablemx_comp//. by rewrite mulmxA mulmxKpV// -[RHS]mulmxA mulmxKpV ?mulmxA. 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)