proposition: Lemma scalemx_eq0 m n a (A : 'M[R]_(m, n)) : (a *: A == 0) = (a == 0) || (A == 0).
proof: Proof. case nz_a: (a == 0) / eqP => [-> | _]; first by rewrite scale0r eqxx. apply/eqP/eqP=> [aA0 | ->]; last exact: scaler0. apply/matrixP=> i j; apply/eqP; move/matrixP/(_ i j)/eqP: aA0. by rewrite !mxE mulf_eq0 nz_a. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg countalg finalg zmodp)