proposition: Lemma mulmx_adjl : forall n (A : 'M_n), adjugate A *m A === (\det A)%:M.
proof: Proof. move=> n A; apply trmx_inj; rewrite -> trmx_mul, trmx_adj, mulmx_adjr. by rewrite -> det_trmx, trmx_scalar; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms