proposition: Lemma det_scalemx : forall n x (A : 'M_n), \det (x *m: A) === x ^+ n * \det A.
proof: Proof. move=> n x A; rewrite/determinant. setoid_rewrite (big_distrr (I:=perm_for_finType (ordinal_finType n)))=>/=. apply eq_bigr => s _; ring_simplify. setoid_rewrite <- rmul_assoc; apply rmul_morph; first by reflexivity. rewrite/scalemx; setoid_rewrite <- (card_ord n) at 4. setoid_rewrite big_split; apply rmul_morph; last by reflexivity. by rewrite <- big_const; apply eq_bigr; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms