proposition: Lemma conj1mx (n : nat) (f : 'M[F]_n) : conjmx 1%:M f = f.
proof: Proof. by rewrite conjumx ?unitmx1// invmx1 mulmx1 mul1mx. 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)