proposition: Lemma det_scalar1 : forall a, \det (a%:M : 'M_1) === a.
proof: Proof. by move=>a; rewrite -> (det_scalar 1 a)=> /=; ring. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms