proposition: Lemma det_scalar : forall n a, \det (a%:M : 'M_n) === a ^+ n.
proof: Proof. move=> n a. transitivity ((a ^+ n) * rI); last by ring. setoid_rewrite <- (det1 n) at 3; setoid_rewrite <- det_scalemx. apply determinant_morph; rewrite <- mulmx_scalar; rewrite <- scalar_mx_mul. by apply scalar_mx_morph; ring. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms