proposition: Lemma conjVmx (n : nat) (V : 'M_n) (f : 'M[F]_n) : V \in unitmx -> conjmx (invmx V) f = invmx V *m f *m V.
proof: Proof. by move=> Vunit; rewrite conjumx ?invmxK ?unitmx_inv. 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)